AltaRica 3.0模型到Promela模型转换与验证方法研究  

A transformation method for AltaRica3.0 to Promela and its verification

作　　者：胡军[1] 陈松[1] 王明明[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机工程与科学》2017年第4期708-716,共9页Computer Engineering & Science

基　　金：国家973计划(2014CB744903);回国留学人员科研启动基金;南京航空航天大学青年科技创新基金(NS2014098)

摘　　要：AltaRica语言用于安全关键系统的建模,其拥有一套完整的建模分析工具,但随着AltaRica3.0的更新,ARC等传统的AltaRica建模分析工具已不再支持,而SPIN作为一个穷尽式模型验证工具被广泛应用。介绍了AltaRica3.0相对于之前版本在表达能力方面的改进,以及其底层模型GTS的基本结构。以AltaRica3.0扁平化为GTS模型的思想为基础,提出了一种AltaRica3.0模型向Promela模型的转换规则。以民用飞机中机轮刹车系统WBS为例,建立了AltaRica3.0模型,并且通过转换规则转为Promela模型。最后根据民用航空标准SAE ARP 4761中对机轮刹车系统的安全性要求,利用SPIN工具对机轮刹车系统的安全属性进行了验证。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 机轮刹车系统 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]