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

Automatic generation of LTL statements for model checking

为优化线性时态逻辑语句的生成过程,减少模型检测的时间,提出一种面向模型检测的基于自然语言处理生成线性时态逻辑验证语句的方法。对需求文档提取关键词,将文档中的数据和可以代表模型中状态的名词进行提取,注释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.