一种AltaRica3.0模型到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模型的转换工作.

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

所属期刊栏目：47

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2020-12-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共14页

页码：73-86