计算机工程与科学2017，Vol.39Issue(4)：708-716,9.DOI:10.3969/j.issn.1007-130X.2017.04.014
AltaRica3.0模型到Promela模型转换与验证方法研究
A transformation method for AltaRica3.0 to Promela and its verification
摘要
Abstract
AltaRica language is used in safety critical systems modeling.It has a complete set of modeling analysis tools.However,with the AltaRica3.0 update,traditional AltaRica modeling and analysis tools like ARC are no longer supportive,and the SPIN as an exhaustive model verification tool is widely used.We briefly introduce the improvement of AltaRica3.0 over the previous version in terms of expressive ability and the basic structure of the underlying model GTS.Based on the idea of AltaRica3.0 flattening into the GTS model,we propose a conversion rule for AltaRica3.0 model transformation to the Promela model.Taking the civil aircraft wheel brake system (WBS) as an example,the AltaRica3.0 model is established and transformed into the Promela model by the conversion rule.Finally,according to the safety requirements of the WBS in 4761,the SPIN tool is used to verify the safety property of the WBS.关键词
安全关键系统/AltaRica3.0/SPIN/机轮刹车系统Key words
safety-critical system/AltaRica3.0/SPIN/wheel brake system分类
信息技术与安全科学引用本文复制引用
胡军,陈松,王明明..AltaRica3.0模型到Promela模型转换与验证方法研究[J].计算机工程与科学,2017,39(4):708-716,9.基金项目
国家973计划(2014CB744903) （2014CB744903）
回国留学人员科研启动基金 （）
南京航空航天大学青年科技创新基金(NS2014098) （NS2014098）
