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