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

• 作者: 王明明 胡军 陈松
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 安全关键系统 AltaRica3.0 SPIN 机轮刹车系统
• 年，卷（期）: 2017,（4）
• 所属期刊栏目: 软件工程
• 页码范围: 708-716
• 页数: 9页
• 分类号: TP311.5
• 字数: 7163字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2017.04.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	胡军	南京航空航天大学计算机科学与技术学院	41	358	10.0	18.0
2	王明明	南京航空航天大学计算机科学与技术学院	9	16	2.0	3.0
3	陈松	南京航空航天大学计算机科学与技术学院	5	15	2.0	3.0