论文部分内容阅读
随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event-B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.
With the rapid increase of software complexity, the traditional test-based approach can not meet the reliability and safety requirements of spacecraft operating systems gradually, and the formal method has become an effective guarantee for the safety and reliability of spacecraft operating systems.Based on the Rodin platform, Event-B is used to formalize the language, and through requirement and design rewriting, the strategy of refinement and refinement is established. The formalized requirements layer and design layer are established for the interrupt management module of SpaceOS2, a space-based embedded operating system. The model Tests and theorem proofs combine to verify the correctness of the model and to satisfy the safety nature.