一种AltaRica3.0模型到NuSMV模型的转换方法  

Transformation Method for AltaRica3.0 Model to NuSMV Model

作　　者：陈朔 胡军[1,2] 唐红英 石梦烨 CHEN Shuo;HU Jun;TANG Hong-ying;SHI Meng-ye(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Collaborative Innovation Center of Novel Software Technology and Industrialization,Nanjing 210007,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]软件新技术与产业化协同创新中心,南京210007

出　　处：《计算机科学》2020年第12期73-86,共14页Computer Science

基　　金：国家重点基础研究发展计划(973计划)(2014CB744904);南京航空航天大学研究生创新基地(实验室)开放基金(kfjj20181607)。

摘　　要：AltaRica 3.0是一类面向复杂关键系统的安全性建模与分析语言,缺乏时态属性的模型检验技术,不支持穷尽式的空间检验,而NuSMV支持穷尽式的模型检验技术,因此对AltaRica 3.0模型进行扩展,提出了基于语言解析器生成器ANTLR(Another Tool for Language Recognition)的AltaRica 3.0模型到NuSMV模型的转换规则和算法。首先,利用ANTLR构建AltaRica 3.0平展化GTS模型的AST(Abstract Syntax Tree);其次,设计语言结构转换规则,显示AltaRica 3.0和NuSMV之间的行为语义对应关系;然后,设计转换算法G2N,在遍历AST时,G2N对结点存储的GTS模型语言信息进行获取和转换,在保留语义的情况下,通过不断地遍历转换过程来获取转换后的NuSMV文件;最后,以需求工程中的4个典型案例为例进行实验分析,验证了G2N的有效性和需求模型的安全性。实验结果表明,G2N算法可以在词法和语法层次上完成AltaRica 3.0模型到NuSMV模型的转换工作。AltaRica 3.0 is a safety modeling and analysis language for safety-critical systems.Because AltaRica 3.0 lacks model checking techniques for temporal properties and does not support exhaustive spaceexamination,NuSMV supports exhaustive model checking techniques.This paper expands AltaRica 3.0,proposes the transformation rules and algorithms of the AltaRica 3.0 model to the NuSMV model based on the language parser generator ANTLR(Another Tool for Language Recognition).Firstly,ASTLR is used to construct the AST(Abstract Syntax Tree)of the AltaRica 3.0 flattening GTS model.Secondly,the language structure transformation rules are designed to show the behavioral semantic correspondence between AltaRica 3.0 and NuSMV.Then,we design the transformation algorithm G2N.When traversing the AST,G2N acquires and transforms the GTS model language information stored by the node,and obtains the transformed NuSMV file through the continuous traversal transformation process while ensuring semantic retention.Finally,example of four typical cases in requirement engineering are used for experimental analysis to verify the effectiveness of the G2N and the safety of the requirement model.Experiments show that the G2N algorithm can complete the conversion of AltaRica 3.0 model to NuSMV model at lexical and grammatical level.

关 键 词：ANTLR AltaRica 3.0 GTS AST NUSMV 模型转换 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]