• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 论文 • 上一篇    下一篇

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

胡军,陈松,王明明   

  1. (南京航空航天大学计算机科学与技术学院,江苏 南京 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   

  1. (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

摘要:

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