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

• 作者: 乔磊 杨桦 谭彦亮
• 来源期刊: 空间控制技术与应用
• 学科: 工学
• 关键词: 任务管理 形式化模型 形式化验证 Event-B
• 年，卷（期）: 2014,（4）
• 页码范围: 57-62
• 页数: 6页
• 分类号: TP311
• 字数: 4040字
• 语种: 中文
• DOI: 10.3969/j.issn.1674-1579.2014.04.011

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谭彦亮		4	15	2.0	3.0
2	杨桦		12	34	4.0	5.0
3	乔磊		17	39	4.0	5.0