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.
相关文章

[1]	马燕燕1，杨志斌1,2，江国华1. 一种SysML模型到AADL模型的自动转换方法[J]. 计算机工程与科学, 2020, 42(03): 456-466.
[2]	宾婧怡，丁旭阳，齐晓铭，陈浩. 面向安全关键应用的多核处理器执行时间波动性分析[J]. 计算机工程与科学, 2019, 41(09): 1541-1550.
[3]	龙士工，王扣武. 多智体系统时序认知规范的SPIN模型检测[J]. J4, 2011, 33(12): 12-16.
[4]	唐郑熠，李 祥. DolevYao攻击者模型的形式化描述[J]. J4, 2010, 32(8): 36-38.
[5]	黄谷,缪力,张大方. 802.11i双向认证协议的模型检查[J]. J4, 2010, 32(4): 25-28.