欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
随着中国航天技术的发展，航天器系统的软件规模越来越大、复杂度越来越高，对航天软件的正确性、可靠性、安全性等提出了更为严格的要求．形式化方法是提高软件可信性的一个重要途径．利用形式化方法Event—B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模，依靠不变式来保证模型的正确性，并且在Rodin平台上对模型进行了形式化验证，结果表明模型是正确的．
英文摘要：
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.
同期刊论文项目
同项目期刊论文
Proving total correctness and generating preconditions for loop programs via symbolic-numeric comput
期刊信息
位置：