面向模型检测的LTL语句自动生成方法  

Automatic generation of LTL statements for model checking

作　　者：段喜龙 陆智伟[1,2] 郑巍 陈晋升[1,2] 樊鑫 肖鹏[1,2] DUAN Xi-long;LU Zhi-wei;ZHENG Wei;CHEN Jin-sheng;FAN Xin;XIAO Peng(School of Software,Nanchang Hangkong University,Nanchang 330063,China;Software Testing and Evaluation Center,Nanchang Hangkong University,Nanchang 330063,China)

机构地区：[1]南昌航空大学软件学院,江西南昌330063 [2]南昌航空大学软件测评中心,江西南昌330063

出　　处：《计算机工程与设计》2023年第8期2337-2344,共8页Computer Engineering and Design

基　　金：国家自然科学基金项目(61867004)。

摘　　要：为优化线性时态逻辑语句的生成过程,减少模型检测的时间,提出一种面向模型检测的基于自然语言处理生成线性时态逻辑验证语句的方法。对需求文档提取关键词,将文档中的数据和可以代表模型中状态的名词进行提取,注释UML模型,对UML模型中的状态进行归类,将模型中的状态分为数据属性类和调用操作类,利用配对的线性时态逻辑格式生成线性时态逻辑,用于软件模型一致性验证。实验结果表明,该方法与ST模型相比可以提高模型检测的效率。To optimize the generation process of linear temporal logic statements,reduce the time of model detection,a model checking oriented method for generating linear temporal logic verification statements based on natural language processing was presented.Keywords were extracted from the requirements document,the data in the document and nouns that represented the state in the model were extracted,the UML model was annotated,the states in the UML model were classified,the states in the model were divided into data attribute classes and call operation classes,and the paired linear temporal logic format was used to generate linear temporal logic for software model consistency verification.Experimental results show that the proposed method can improve the efficiency of model detection compared with ST model.

关 键 词：自然语言处理 模型一致性 线性时态逻辑 UML模型 形式化验证工具 模型验证 模型注释 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]