Abstract:  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.