Abstract: With the rapid growth of software complexity, the traditional testing method is gradually difficult to meet the reliability and security requirements of spacecraft operating system. Formal method is gradually becoming an effective guarantee for spacecraft operating system security and reliability. Based on the Rodin platform, using EventB formal language, through the requirements and design rewrite and formulate the refinement strategy and stepwise refinement method, the requirement layer and design layer formal model is established for the interruptmanagement module of the embedded operating system SpaceOS2. Model checking and theorem proving are combined to verify the validity and safety of the model.

Key words: interruptmanagement, formal verification, EventB, refinement