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

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

作　　者：王若川[1] 杨孟飞[1,2] 乔磊[1] 

机构地区：[1]北京控制工程研究所,北京100190 [2]中国空间技术研究院,北京100094

出　　处：《空间控制技术与应用》2014年第4期52-56,共5页Aerospace Control and Application

基　　金：国家自然科学基金资助项目(91118007)

摘　　要：时序正确性问题一直以来都是航天嵌入式软件的热点、难点问题.运用时间自动机理论,对某星载操作系统的中断管理进行了建模,同时对与操作系统行为存在交互的环境进行了建模,以描述完整的中断管理过程.利用模型检测工具箱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.

关 键 词：中断管理 时间自动机 形式化验证 建模 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]