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

作     者：陈朔 胡军 唐红英 石梦烨 CHEN Shuo;HU Jun;TANG Hong-ying;SHI Meng-ye

作者机构：南京航空航天大学计算机科学与技术学院南京211106 软件新技术与产业化协同创新中心南京210007 

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

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2020年第47卷第12期

页      码：73-86页

摘      要：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模型的转换工作。

主 题 词：ANTLR AltaRica 3.0 GTS AST NuSMV 模型转换 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.11896/jsjkx.190400035

馆 藏 号：203997126...