10.3969/j.issn.1007-130X.2017.04.014
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