基于Event B的中断管理需求和设计形式化建模与验证方法

随着软件复杂度的迅速增长，传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求，形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台，采用Event B形式化语言，通过需求和设计重写、制定精化策略并逐步精化的方法，对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型，将模型检验和定理证明相结合，验证模型的正确性并且满足安全性质.

Formal Modeling and Verification Method of Interrupt Management Requirement and Design Based on Event B

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.