基于有限状态机的操作系统需求层形式化验证

操作系统是航天器必备的基本软件，操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障，但仍存在不能完全排除缺陷的情况，因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分，本文在分析操作系统需求的基础上，采用有限状态机在操作系统需求层进行形式化描述，并针对应用在某航天器上的SpaceOS2在需求层进行了建模，相应地在定理证明工具Coq中进行了描述建模；然后定义了六条操作系统应满足的全局性质并进行了形式化描述，给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的，为进一步全面形式化验证奠定了基础.

Formal Verification of Operating System Requirements Layer#br# Based on Finite State Machine#br#

The operating system is the basic software necessary for the spacecraft. The reliability and security of the operating system are directly related to the success or failure of the aerospace model mission. Although various methods have been used to guarantee the reliability and security of the operating system, there are still cases where the defects cannot be completely eliminated. Therefore, it is imperative to conduct formal verification research on space operating systems. The verification of requirement layer is a part of the formal verification of the operating system. Based on the analysis of the operating system requirements,a method of finite state machine is used to formally describe in the demand layer and applied to a spacecraft. SpaceOS2 is modeled at the requirements level, and correspondingly described in the theorem proving tool Coq; then formal definitions are made for some global properties, and the machine checkable proof that the system model satisfies these properties is given. The proof result shows that the finite state machine method is feasible to formally verify the operating system requirements layer and lays the foundation for further comprehensive formal verification.