%0 Journal Article %T SpaceOS中若干全局性质的形式化描述和验证 %A 乔磊 %A 付明 %A 冯新宇 %A 顾海博 %J 中山大学学报(自然科学版) %D 2019 %X 摘要 SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素.SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为SpaceOS内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证SpaceOS在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成 %K SpaceOS %K 形式化验证 %K 全局性质 %K 操作系统内核 %K Coq %U http://xwxt.sict.ac.cn/CN/abstract/abstract4801.shtml