资料下载
×
AltaRica3.0模型到NuSMVP模型的转换规则和算法
消耗积分:0 |
格式:pdf |
大小:5.86 MB |
2021-04-23
分享资料个
Altarica3.0是一类面向复杂关键系统的安全性建模与分析语言，缺乏时态属性的模型检验技术，不支持穷尽式的空间检验，而NuSM攴持穷尽式的模型检验技术，因此对Δlτ a rica3.θ模型进行扩展，提岀了基于语言解析器生成器 ANTLR（ Another Tool for Language recognition）的 Alta rica3.0模型到NusMⅤ模型的转换规则和算法。首先，利用 ANTLR构建Alta rica3.0平展化GTS模型的AST（ Abstract Syntax Tree）;其次，设计语言结构转换规则，显示 Altarica3.0和 NUSMV之间的行为语义对应关系;然后，设计转换算法G2N，在遍历AST时，G2N对结点存储的GTS模型语言信息进行获取和转换，在保留语义的情况下，通过不断地遍历转换过程来获取转换后的 NUSMV文件;最后，以需求工程中的4个典型案例为例进行实验分析，验证了（2N的有效性和需求模型的安全性。实验结果表明，G2N算法可以在词法和语法层次上完成Δ Italicα3.0模型到NuSMⅤ模型的转换工作。
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
评论(0)
发评论
- 相关下载
- 相关文章
