基于模型检验的需求不一致研究

Research on requirement inconsistent method based on model checking

为在软件需求分析阶段获得易于理解且一致性需求,在现有的研究基础上,提出一种基于自然语言与模型检验相结合的方法。将自然语言描述的需求按照子句的相似度进行划分,提取关键词转换成自动机模型,对转换后的模型使用SMV语言描述并用模型检验工具和方法对模型进行分析和验证,通过乘坐电梯的案例对此方法进行实验验证。实验结果表明,该方法能够高效验证系统需求并能根据反例修正可能出现的错误,为系统需求模型的一致性验证提供一种思路。

To obtain consistent requirements that are easy to understand in the stage of software requirement analysis,a method based on natural language and model checking was proposed on the basis of the existing research.The requirements of natural language description were divided according to the similarity of clauses,and the keywords were extracted into automatic machine models.The transformed model was described through SMV language and analyzed and verified using model checking tools and methods.An elevator case was used to analyze and verify the proposed method.The results indicate that the proposed method can efficiently verify the system requirements and correct the possible errors according to the counter examples,it is a creative approach to verify the consistency of the system requirement model.