AltaRica3.0模型到Promela模型转换与验证方法研究

摘要：

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、机轮刹车系统

所属期刊栏目：39

分类号：TP311.5(计算技术、计算机技术)

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

在线出版日期：2017-05-23（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：708-716