中国科技核心期刊

中文核心期刊

CSCD来源期刊

空间控制技术与应用 ›› 2014, Vol. 40 ›› Issue (4): 52-56.doi: 10.3969/j.issn.1674-1579.2014.04.010

• 技术交流 • 上一篇    下一篇

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

  

  • 出版日期:2014-08-20 发布日期:2014-08-20

Modeling and Verification of Operating System Interrupt Management Based on Timed Automata

  • Online:2014-08-20 Published:2014-08-20

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

关键词: 时间自动机, 形式化验证, 建模

Abstract: 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 tool Uppaal, the performances of interrupt management are verified, including the reachability, the safety, the liveness and the correctness of service behavior.

Key words: interrupt management, timed automata, formal verification, modeling

中图分类号: 

  •