面向模型检测的LTL语句自动生成方法 |
| |
引用本文: | 段喜龙,陆智伟,郑巍,陈晋升,樊鑫,肖鹏.面向模型检测的LTL语句自动生成方法[J].计算机工程与设计,2023(8):2337-2344. |
| |
作者姓名: | 段喜龙 陆智伟 郑巍 陈晋升 樊鑫 肖鹏 |
| |
作者单位: | 1. 南昌航空大学软件学院;2. 南昌航空大学软件测评中心 |
| |
基金项目: | 国家自然科学基金项目(61867004); |
| |
摘 要: | 为优化线性时态逻辑语句的生成过程,减少模型检测的时间,提出一种面向模型检测的基于自然语言处理生成线性时态逻辑验证语句的方法。对需求文档提取关键词,将文档中的数据和可以代表模型中状态的名词进行提取,注释UML模型,对UML模型中的状态进行归类,将模型中的状态分为数据属性类和调用操作类,利用配对的线性时态逻辑格式生成线性时态逻辑,用于软件模型一致性验证。实验结果表明,该方法与ST模型相比可以提高模型检测的效率。
|
关 键 词: | 自然语言处理 模型一致性 线性时态逻辑 UML模型 形式化验证工具 模型验证 模型注释 |
|
|