论文摘要
操作系统是航天器必备的基本软件,操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障,但仍存在不能完全排除缺陷的情况,因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分,本文在分析操作系统需求的基础上,采用有限状态机在操作系统需求层进行形式化描述,并针对应用在某航天器上的SpaceOS2在需求层进行了建模,相应地在定理证明工具Coq中进行了描述建模;然后定义了六条操作系统应满足的全局性质并进行了形式化描述,给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的,为进一步全面形式化验证奠定了基础.
论文目录
文章来源
类型: 期刊论文
作者: 张锦坤,杨孟飞,乔磊,杨桦,刘波
关键词: 操作系统,形式化验证,系统需求,有限状态机
来源: 空间控制技术与应用 2019年02期
年度: 2019
分类: 工程科技Ⅱ辑
专业: 航空航天科学与工程
单位: 北京控制工程研究所,中国空间技术研究院,中国科学院软件研究所计算机科学国家重点实验室
基金: 国家自然科学基金资助项目(61502031,61632005)~~
分类号: V446
页码: 48-55
总页数: 8
文件大小: 236K
下载量: 192