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

作     者：顾海博 付明 乔磊 冯新宇 GU Hai-bo;FU Ming;QIAO Lei;FENG Xin-yu

作者机构：中国科学技术大学计算机科学与技术学院合肥230027 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123 华为上海研究所2012实验室-OS内核实验室上海201206 北京控制工程研究所北京100190 南京大学计算机软件新技术国家重点实验室南京210023 

基　　金：国家自然科学基金项目(61632005 61502031)资助 

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2019年第40卷第1期

页      码：141-148页

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

主 题 词：SpaceOS 形式化验证 全局性质 操作系统内核 Coq 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1000-1220.2019.01.026

馆 藏 号：203453924...