基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

谭彦亮; 杨桦; 乔磊

首页> 中文期刊>空间控制技术与应用 >基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

开具论文收录证明 >>

期刊封面封底目录下载 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

随着中国航天技术的发展,航天器系统的软件规模越来越大、复杂度越来越高,对航天软件的正确性、可靠性、安全性等提出了更为严格的要求.形式化方法是提高软件可信性的一个重要途径.利用形式化方法Event-B对嵌入式操作系统SpaceOS2的任务管理模块的进行需求建模,依靠不变式来保证模型的正确性,并且在Rodin平台上对模型进行了形式化验证,结果表明模型是正确的.

著录项

来源
《空间控制技术与应用》|2014年第4期|57-62|共6页
作者
谭彦亮; 杨桦; 乔磊;
展开▼
作者单位

北京控制工程研究所,北京100190;

北京控制工程研究所,北京100190;

北京控制工程研究所,北京100190;

展开▼
原文格式 PDF
正文语种 chi
中图分类程序设计、软件工程;
关键词
任务管理; 形式化模型; 形式化验证; Event-B;
入库时间 2022-08-17 18:30:15

相似文献

中文文献
外文文献
专利

1. 基于Event-B的中断管理需求和设计形式化建模与验证方法 [J] . 周育逵 ,杨桦 ,乔磊 . 空间控制技术与应用 . 2017,第003期
2. 基于Coq的操作系统任务管理需求层建模及验证 [J] . 姜菁菁 ,乔磊 ,杨孟飞 . 软件学报 . 2020,第008期
3. 基于Event-B方法的需求建模及验证 [J] . 史逸轩 . 忻州师范学院学报 . 2019,第002期
4. 基于Event-B的细化需求建模及验证 [J] . Shi Yi-xuan ,Wang Hong-bin . 长治学院学报 . 2019,第002期
5. 基于有限状态机的操作系统需求层形式化验证 [J] . 张锦坤 ,杨孟飞 ,乔磊 . 空间控制技术与应用 . 2019,第002期
6. SpaceOS2汇编代码的形式化建模与验证方法 [C] . 周育逵 ,乔磊 ,杨桦 . 2018年第十五届全国工业控制计算机学术年会 . -1
7. 基于Event-B的软件需求形式化建模技术的研究 [A] . 陈志慧 . 2013

基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证

摘要

著录项

相似文献

相关主题

期刊订阅