空间控制技术与应用
空間控製技術與應用
공간공제기술여응용
AEROSPACE CONTROL AND APPLICATION
2014年
4期
52-56
,共5页
中断管理%时间自动机%形式化验证%建模
中斷管理%時間自動機%形式化驗證%建模
중단관리%시간자동궤%형식화험증%건모
interrupt management%timed automata%formal verification%modeling
时序正确性问题一直以来都是航天嵌入式软件的热点、难点问题.运用时间自动机理论,对某星载操作系统的中断管理进行了建模,同时对与操作系统行为存在交互的环境进行了建模,以描述完整的中断管理过程.利用模型检测工具箱Uppaal验证了中断管理模块的状态可达性、安全性、活性等方面的性质,证明了其服务行为的正确性.
時序正確性問題一直以來都是航天嵌入式軟件的熱點、難點問題.運用時間自動機理論,對某星載操作繫統的中斷管理進行瞭建模,同時對與操作繫統行為存在交互的環境進行瞭建模,以描述完整的中斷管理過程.利用模型檢測工具箱Uppaal驗證瞭中斷管理模塊的狀態可達性、安全性、活性等方麵的性質,證明瞭其服務行為的正確性.
시서정학성문제일직이래도시항천감입식연건적열점、난점문제.운용시간자동궤이론,대모성재조작계통적중단관리진행료건모,동시대여조작계통행위존재교호적배경진행료건모,이묘술완정적중단관리과정.이용모형검측공구상Uppaal험증료중단관리모괴적상태가체성、안전성、활성등방면적성질,증명료기복무행위적정학성.
