| 基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证 |
| |
| 引用本文： | 谭彦亮,杨桦,乔磊.基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证[J].空间控制技术与应用,2014(4):57-62. |
| |
| 作者姓名： | 谭彦亮 杨桦 乔磊 |
| |
| 作者单位： | 北京控制工程研究所; |
| |
| 基金项目： | 国家自然科学基金资助项目(91118007) |
| |
| 摘 要： | 随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法 Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的.
|
| 关 键 词： | 任务管理 形式化模型 形式化验证 Event—B |
Formal Modeling and Verification of Task-Management Requirement for SpaceOS2 Based on Event-B |
| |
| TAN Yanliang,YANG Hua,QIAO Lei.Formal Modeling and Verification of Task-Management Requirement for SpaceOS2 Based on Event-B[J].Aerospace Contrd and Application,2014(4):57-62. |
| |
| Authors: | TAN Yanliang YANG Hua QIAO Lei |
| |
| Institution: | (Beijing Institute of Control Engineering, Beijing 100190, China) |
| |
| Abstract: | With the development of space technology in China, the software applied in spacecraft becomes more complex and larger in scale. It is necessary to improve the correctness, reliability and security of software to achieve a high level. Among the approaches, the formal method is an important one. A formal method based on Event-B is introduced to describe the requirement for task model of SpaceOS2. The cor- rectness of this model is formally guaranteed via virtual of invariants. The correctness of the model is veri- fied by using the Rodin platform. |
| |
| Keywords: | task management formal model formal verification Event-B |
| 本文献已被 CNKI 维普 等数据库收录！ |
