周育逵,杨 桦,乔 磊

(北京控制工程研究所,北京 100190)



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

周育逵,杨 桦,乔 磊

(北京控制工程研究所,北京 100190)

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

0 引 言

在航空航天领域，航天器操作系统的安全性因其生命期长，结构复杂，稳定性要求高和出错代价高昂开始引起了广泛的关注.操作系统由于其复杂性，其正确性很难用定量的方式进行描述和说明，由于操作系统软件在各类航天器计算机应用中的核心地位，其可靠性至关重要.随着软件复杂度的迅速增长，传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求，形式化方法逐渐成为航天器操作系统安全可靠性的有效保障，采用形式化的方法对操作系统进行设计和验证[1-2]已经得到国际学术界的广泛重视.

形式化方法[3]是建立在严格数学基础上的用以对软硬件系统进行说明、设计和验证的语言、技术和工具……