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

作者：陈朔; 胡军^*; 唐红英; 石梦烨

来源：计算机科学, 2020, 47(12): 73-86.

• ANTLR
• AltaRica 3.0
• GTS
• AST
• NuSMV
• 模型转换

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

• 单位
  南京航空航天大学