中文摘要：

为了达到经过形式化验证分区操作系统内核隔离性质的目标,采取形式化方法描述系统的顶层规范设计中描述隔离性质需求,通过将航空电子应用软件标准接口ARINC653与GWV定理相结合,实现了对分区操作系统需要满足的隔离性质的抽象描述,并通过使用类Z/Z＋＋作为形式化描述语言。

英文摘要：

In order to verification the separation property of a partition operation system kernel which could be verified formally.We have taken formal method to specify the separation property requirement in the top-level design of our system.Combining the standard interface for avionics applications ARINC653and GWV Theorem,our work realized the abstract of separation properties that partition operating system need to satisfy,and use a Z/Z＋＋like language for the formal specification.