摘要
时序正确性问题一直以来都是航天嵌入式软件的热点、难点问题.运用时间自动机理论,对某星载操作系统的中断管理进行了建模,同时对与操作系统行为存在交互的环境进行了建模,以描述完整的中断管理过程.利用模型检测工具箱Uppaal验证了中断管理模块的状态可达性、安全性、活性等方面的性质,证明了其服务行为的正确性.
The temporal correctness has always been a hot-spot and difficult problem in the field of space embedded software. With the theory of timed automata, the interrupt management of a certain on-board operating system and the environment interacting with it are modeled respectively to describe the whole interrupt management process. By using the model-checking toot Uppaal, the performances of interrupt management are verified, including the reachability, the safety, the liveness and the correctness of serv- ice behavior.
出处
《空间控制技术与应用》
2014年第4期52-56,共5页
Aerospace Control and Application
基金
国家自然科学基金资助项目(91118007)
关键词
中断管理
时间自动机
形式化验证
建模
interrupt management
timed automata
formal verification
modeling
