SpaceOS中若干全局性质的形式化描述和验证

摘要 SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素.SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为SpaceOS内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证SpaceOS在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成