【摘 要】
：
SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素. SpaceOS在
【机 构】
：
中国科学技术大学计算机科学与技术学院; 中国科学技术大学苏州研究院软件安全实验室; 华为上海研究所2012实验室-OS内核实验室; 北京控制工程研究所; 南京大
【基金项目】
：
国家自然科学基金项目(61632005,61502031)资助
论文部分内容阅读
SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素. SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为SpaceOS内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证SpaceOS在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成.
其他文献
针对复杂背景条件下声目标的自动识别问题,设计了一种基于模糊综合评判的声目标识别系统.该系统在对典型战场声目标特征进行充分提取与选择的基础上,建立反映目标类属特征的隶属函数库,采用先进的模糊综合评判技术实现对目标的可靠识别.对特征提取与选择、隶属函数确定、模糊评判、原理样机实现等关键问题进行了详细的讨论.实测检验表明,该系统对战场声目标具有良好的识别分类效果.
河源电厂2号机组系由哈尔滨汽轮机厂与日本三菱公司联合设计生产的超超临界600MW汽轮机,型号为CLN600-25/600/600。机组设有一个高中压缸和一个低压缸,及发电机和集电环,共7
煤粉炉以自身的燃烧优势被广泛应用于集中供热锅炉房。煤粉也有弱点,其易氧化自燃与爆炸特性是设计工作中的难点与重点。本文针对煤粉特性、爆炸机理及预防措施进行了简要叙