桂林电子科技大学学报
桂林電子科技大學學報
계림전자과기대학학보
JOURNAL OF GUILIN UNIVERSITY OF ELECTRONIC TECHNOLOGY
2011年
2期
125-129
,共5页
实时系统%ASEHA%时钟约束%模型检测%UPPAAL
實時繫統%ASEHA%時鐘約束%模型檢測%UPPAAL
실시계통%ASEHA%시종약속%모형검측%UPPAAL
为了有效地分析实时系统,在原计算模型的基础上,引入了时钟变量,在迁移上增加了时钟约束,扩展了异步扩展层次自动机的语义.运用基于时间扩展的ASEHA,分析了ATM系统,建立了用户和ATM的模型,并使用模型检测工具UPPAAL对模型进行验证,从无死锁、活性及可达性性质出发,验证了ATM系统的安全性.实验表明,提出的基于时间扩展的ASEHA能够降低系统分析的复杂性,有助于实时系统的建模与验证.
為瞭有效地分析實時繫統,在原計算模型的基礎上,引入瞭時鐘變量,在遷移上增加瞭時鐘約束,擴展瞭異步擴展層次自動機的語義.運用基于時間擴展的ASEHA,分析瞭ATM繫統,建立瞭用戶和ATM的模型,併使用模型檢測工具UPPAAL對模型進行驗證,從無死鎖、活性及可達性性質齣髮,驗證瞭ATM繫統的安全性.實驗錶明,提齣的基于時間擴展的ASEHA能夠降低繫統分析的複雜性,有助于實時繫統的建模與驗證.
위료유효지분석실시계통,재원계산모형적기출상,인입료시종변량,재천이상증가료시종약속,확전료이보확전층차자동궤적어의.운용기우시간확전적ASEHA,분석료ATM계통,건립료용호화ATM적모형,병사용모형검측공구UPPAAL대모형진행험증,종무사쇄、활성급가체성성질출발,험증료ATM계통적안전성.실험표명,제출적기우시간확전적ASEHA능구강저계통분석적복잡성,유조우실시계통적건모여험증.
