基于时间自动机的操作系统中断管理建模与验证

• 作者: 乔磊 杨孟飞 王若川
• 来源期刊: 空间控制技术与应用
• 学科: 工学
• 关键词: 中断管理 时间自动机 形式化验证 建模
• 年，卷（期）: 2014,（4）
• 页码范围: 52-56
• 页数: 5页
• 分类号: TP301
• 字数: 3541字
• 语种: 中文
• DOI: 10.3969/j.issn.1674-1579.2014.04.010

摘要

时序正确性问题一直以来都是航天嵌入式软件的热点、难点问题.运用时间自动机理论,对某星载操作系统的中断管理进行了建模,同时对与操作系统行为存在交互的环境进行了建模,以描述完整的中断管理过程.利用模型检测工具箱Uppaal验证了中断管理模块的状态可达性、安全性、活性等方面的性质,证明了其服务行为的正确性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨孟飞		18	120	3.0	10.0
5	乔磊		17	39	4.0	5.0
6	王若川		2	3	1.0	1.0