|
|||||
|
|
| 基于时间自动机的操作系统中断管理建模与验证 | |
| 引用本文： | 王若川,杨孟飞,乔磊.基于时间自动机的操作系统中断管理建模与验证[J].空间控制技术与应用,2014(4). |
| 作者姓名： | 王若川 杨孟飞 乔磊 |
| 作者单位： | 北京控制工程研究所;中国空间技术研究院; |
| 基金项目： | 国家自然科学基金资助项目(91118007) |
| 摘 要： | 时序正确性问题一直以来都是航天嵌入式软件的热点、难点问题.运用时间自动机理论,对某星载操作系统的中断管理进行了建模,同时对与操作系统行为存在交互的环境进行了建模,以描述完整的中断管理过程.利用模型检测工具箱Uppaal验证了中断管理模块的状态可达性、安全性、活性等方面的性质,证明了其服务行为的正确性. |
| 关 键 词： | 中断管理 时间自动机 形式化验证 建模 |
| 本文献已被 CNKI 等数据库收录！ | |