关键词: 任务管理, 形式化模型, 形式化验证, Event-B

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 correctness of this model is formally guaranteed via virtual of invariants. The correctness of the model is verified by using the Rodin platform.

Key words: task management;formal model;formal verification, Event-B