Formal Modeling and Verification of the Design Layer of Space Operating Systems

The operating system is an essential basic software for spacecraft, and its reliability and safety are directly related to the success or failure of aerospace missions. Although various methods have been used to ensure the reliability and security of operating systems, there are still situations where defects cannot be completely eliminated. Therefore, it is imperative to conduct formal verification research on space operating systems. The verification of design layer is a part of formal verification of operating system. Based on the analysis of task management module of operating system, this paper proposes a formal modeling method using finite state machine at the design layer, and uses this method to model SpaceOS2 applied on a spacecraft at the design layer, and correspondingly describes the modeling in the theorem proving tool Coq; then, some local property are formally defined, and the proof that the system model satisfies these properties is given. The results show that SpaceOS2 meets the proposed local property at the design layer, which lays the foundation for further comprehensive formal verification.