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

计算机工程与科学

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

胡军，陈松，王明明

（南京航空航天大学计算机科学与技术学院,江苏南京 210016）

收稿日期:2016-12-20 修回日期:2017-02-25 出版日期:2017-04-25 发布日期:2017-04-25
基金资助:
国家973计划(2014CB744903);回国留学人员科研启动基金;南京航空航天大学青年科技创新基金(NS2014098)

A transformation method for AltaRica3.0

to Promela and its verification

HU Jun，CHEN Song，WANG Ming-ming

（College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China）

Received:2016-12-20 Revised:2017-02-25 Online:2017-04-25 Published:2017-04-25

摘要/Abstract

摘要：

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

关键词: 安全关键系统, AltaRica3.0, SPIN, 机轮刹车系统

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.

Key words: safety-critical system, AltaRica3.0, SPIN, wheel brake system

胡军，陈松，王明明. AltaRica 3.0模型到Promela模型转换与验证方法研究[J]. 计算机工程与科学.

HU Jun，CHEN Song，WANG Ming-ming.

A transformation method for AltaRica3.0

to Promela and its verification

[J]. Computer Engineering & Science.

[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.