%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