基于Event-B的中断管理需求和设计形式化建模与验证方法

• 作者: 乔磊 周育逵 杨桦
• 来源期刊: 空间控制技术与应用
• 学科: 工学
• 关键词: 中断管理 形式化验证 Event-B 精化
• 年，卷（期）: 2017,（3）
• 所属期刊栏目: 技术交流
• 页码范围: 71-78
• 页数: 8页
• 分类号: TP311
• 字数: 5567字
• 语种: 中文
• DOI: 10.3969/j.issn.1674-1579.2017.03.012

摘要

随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event-B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨桦		12	34	4.0	5.0
2	乔磊		17	39	4.0	5.0
3	周育逵		1	2	1.0	1.0