论文基于模型检验需求不一致研究与消解

基于模型检验的需求不一致与冲突消解的研究 摘 要 随着软件规模的增大，软件需求分析也变的越来越重要，使用目前的一些建模和分析方法有一定的效果，但在理论和实践方面还存在着描述的需求不一致、变更困难等问题，本文针对这些问题进行了以下研究：
为了发现需求描述中的不一致问题，首先使用自然语言对需求描述进行相似度计算，为模型检验提供定位策略。然后，通过对自然语言的分解提取，形成自动机模型，自动机模型和属性规约同时交由模型检验工具进行验证，最后，由模型检验工具得出与属性规约一致或者不一致的地方。

为了对发现的需求冲突进行消解，首先对不同的需求进行分类，分成功能性需求和非功能性需求，对用功能性需求采用需求关联度的方法进行消解，对于非功能性需求采用代价权衡策略进行冲突消解。最后通过一个样例说明了提出方法的可靠性，因此，本文在提高软件需求质量方面有一定的理论意义和应用价值。

关键词：模型检验；

需求相似度；

需求关联度；
代价权衡策略 Research on requirement inconsistency and conflict resolution based on model checking Abstract With the increase of software scale, software requirement analysis is becoming more and more important. Using some current modeling and analysis methods has certain effect, but there are still some problems in theory and practice, such as inconsistent requirements and change difficulties. This paper studies these problems as follows: In order to find the inconsistencies in the requirement description, we first use natural language to calculate the similarity of the requirement description and provide the positioning strategy for the model test. Then, through the decomposition and extraction of natural language, an automata model is formed. The automata model and the attribute specification are submitted to the model checking tool for verification at the same time. Finally, the consistency or inconsistency between the model checking tool and the attribute specification is obtained. In order to resolve the conflict of requirements, firstly, different requirements are classified into functional requirements and non functional requirements. The functional requirements are resolved by the method of demand relevance, and the non functional requirements are resolved by the cost trade-off strategy. Finally, an example is given to show the reliability of the proposed method. Therefore, this paper has certain theoretical significance and application value in improving the quality of software requirements. Keywords：
Model Checking; Requirement Similarity;Requirement Relevance; Cost Tradeoff strategy 目录 第一章 引言 1 1.1 研究背景及意义 1 1.2 国内外研究现状 3 1.3论文的研究内容及创新点 4 1.3.1 论文的主要研究内容 4 1.3.2 论文的主要创新点 5 1.4 本文的组织结构 5 第二章 框架研究与建立 6 2.1 需求不一致问题概述 6 2.1.1 需求不一致相关研究 6 2.2 需求冲突消解问题概述 7 2.2.1 需求冲突消解相关研究 7 2.3 研究整体框架 8 2.4 小结 9 第三章 基于模型检验的需求不一致研究 10 3.1 基于自然语言的需求描述与转换 11 3.1.1 需求子句相似度模型 11 3.1.2 自动机模型 14 3.1.3 从自然语言提取到自动机模型 15 3.2 基于模型检验的需求不一致 17 3.2.1 模型检验及相关定义 19 3.2.2 模型检验实现 20 3.2.3 模型转换 22 3.2.4反例及其作用 23 3.3 小结 25 第四章 需求冲突消解的研究与实现 26 4.1 概述 26 4.2 功能性需求冲突消解 27 4.2.1 需求关联性与一致化程度 27 4.2.2 基于需求关联度冲突消解 28 4.3 非功能性需求消解 30 4.3.1 代价权衡分析 30 4.3.2 不可度量策略 30 4.3.3 可度量策略 32 4.4 小结 36 第五章 案例分析 37 5.1电梯模型的描述与建模 37 5.2 属性规约提取与验证 41 5.3 需求冲突消解 43 5.4小结 44 第六章 总结与展望 44 6.1 总结 44 6.2 展望 45 参考文献 46 攻读学位期间的研究成果 48 附录1 农夫过河问题SMV语言描述 49 致 谢 51 学位论文独创性声明 52 学位论文知识产权权属声明 53 第一章 引言 1.1 研究背景及意义 在软件开发初期，由于软件规模小，功能简单，软件开发阶段往往只注重编码工作，随着计算机软件规模的不断扩大，功能逐渐复杂，原来的只注重编码的方式不能再满足日益复杂的需求，“软件危机”开始爆发。自此，人们才开始认识到软件工程中的技术和方法在软件开发过程中的重要性。据有关资料统计，软件项目中40%~60%都是在需求阶段埋下的祸根，其主要原因是人们容易忽略了很多与需求相关的问题。而这一系列的问题很容易导致后续阶段出现严重的错误设计。Boehm和Papaccio在1988年的研究报告中表明[1]，如果在需求定义过程中找出并修改一个基于需求的问题的代价为1或2，在设计阶段的这个代价就上升 到5，编码时代价是10，单元测试时是20，而在系统提交后这个代价就变成200。可以看出，如何正确对待软件开发阶段需求问题已经变得非常重要了。

人们对软件质量的要求越来越高，需求工程这一软件工程的一个重要分支便应运而生。需求工程着重于研究利用有效的技术，工程化的方法进行描述分析，需求工程的最终目的是通过一系列的科学有效的方法获取高质量的软件需求[2]，一般意义上的软件工程包含需求开发和需求管理两个部分。其中，需求开发又包含需求获取、需求分析与建模、编写软件规格说明、需求验证。需求管理包含需求跟踪和需求变更控制等。在整个软件开发的生命周期中，软件需求的获取和分析是十分重要的部分也是首要解决的问题。软件需求是指用户解决问题或达到目标所需条件或权能，是反应系统或系统部件要满足的合同、标准、规模或其他正式规定文档所需具有的条件或权能的文档说明。它一般包括功能性需求及非功能性需求[3]。综上，软件需求应是以一种清晰、简明、一致且无二义性的方式对一个待开发系统中的各个方面进行描述的集合。

在软件开发中，尽管软件设计和实现过程的错误会导致软件项目的失败，但当软件需求与分析存在缺陷时，则无论设计和实现过程如何，软件都必然存在错误，只有当获取分析并形成正确无二义性的需求时，才更有可能使得软件项目成功。在软件需求分析阶段，由于涉众复杂，需求变更频繁，系统复杂度不断提高，导致需求分析变的越来越困难。其中，需求的不一致的存在会导致软件系统的混乱甚至是错误。在许多复杂的软件系统中都会大概率地出现需求不一致。一般来说出现需求不一致的原因可以归纳为两点：一是在需求描述阶段，由于来自不同视点的不同的利益相关者对同一事物的描述可能存在差异，二是由于在需求迭代和完善性维护中，不断增加的新需求与原来的旧需求之间可能存在不一致。对于任何一个复杂系统来说，不论是自身描 述的不一致还是新的需求带来的不一致问题都会给系统带了一系列的问题。

需求不一致的出现会给系统出现矛盾甚至是错误，目前有大量的专家学者研究需求不一致的问题，一般分为三个方面，需求不一致的检测和诊断；
需求不一致的处理；
需求不一致的度量和评估。对于需求分析中的需求不一致问题，需求分析者往往需要花费大量时间并使用各种方法来查找其中的问题，然后去修正需求分析中出现的错误。使用目前这些方法进行需求分析和处理时还是不可避免的存在一些问题：
（1）需求描述过于形式化难以保障用户和分析人员的理解 在需求描述阶段，使用一些形式化方法如VDM、Z方法、B方法等，虽然比当前的统一建模语言UML拥有更加严格的语义和推理机制。但是研究发现，与需求描述接触最多的还是普通的需求分析者，他们大多没有非常专业的数学知识，这样不利于需求模型的构建。

（2）难以给需求潜在的需求不一致进行定位 当遇到大规模需求描述时，纯手动的方法已经几乎不可能完成需求文档的编写，需要用到自动或半自动的方法，但是在这些方法中很少由涉及到有关需求不一致的定位策略。实际上，在大规模需求描述中，我们需要排除很多无关因素来保证我们的需求描述的正确性和一致性。

（3）发现和消除不一致的方法过于单一 在目前的软件开发中，对系统需求的持续更改以及不断提出新需求的情况更加频繁[4]。而对于这些需求不一致的发现和消除方法过于单一，传统消除不一致的方法一般侧重于某一个点，实际上随着系统的复杂，影响需求不一致的因素越来越多，只从单一因素考虑消除不一致不能适应复杂系统的变化。

本文主要研究在需求获取和需求分析阶段如何发现和消除需求不一致问题。通过对需求分析阶段的需求描述进行分析并建立模型，实现发现需求不一致性，并且根据发现的不一致运用相应的策略进行消解，旨在通过本文的方法获取清晰、完整、一致性的系统需求。通过分析现有的研究方法优缺点，提出一种基于模型检验的需求不一致的分析方法，从自然语言描述的需求中提取出出自动机模型，并使用模型转换的方法转换成模型检验能够识别的模型，使用模型检验的工具自动遍历模型，得出可能的不一致的地方，并在此基础上对发现的不一致需求结合需求关联度和代价权衡提出消解策略，结合其类别和权衡代价进行需求冲突的消解。

本论文开展的此研究课题具有以下几个方面的重要意义：
（1）使用自然语言描述和需求相似度算法，给潜在的需求不一致提供定位策略。

（2）使用模型检验的方法自动遍历由自然语言形成的自动机模型，得出与预期不一致的地方。

（3）对需求进行分类，使用需求关联度和代价权衡策略对发现的需求冲突提供消解方法和策略。

1.2 国内外研究现状 近些年来，关于需求不一致的及需求冲突的消解问题已有很多方面的研究。

在研究需求不一致问题上，Nuseibe[5]等人提出了一个需求不一致的管理框架，可以说是具有代表性的工作，在这个框架中，提出的一致性规则是至关重要的，因为需求不一致都是相对于这些规则而言的。主要分为几类，一是采用经典逻辑的方法通过检测逻辑表达式的值来发现需求不一致[6]，此类方法把需求描述和逻辑断言进行关联，运用逻辑推理的方法找出逻辑断言中的矛盾，进而表示出需求描述中矛盾。

二是采用模型检验的方式来检测需求规格说明中的错误，Heitmeyer C L[7]提出一个基于模型检验的检测需求不一致的框架，此种方法将需求表示为状态变量，通过自动遍历状态变量的取值和预期是否相同来检测需求不一致。三是基于目标的方法，先把初始需求定义为一个目标，通过对这个目标的分解，抽象和求精等以及这个目标的子目标之间的关联和约束等发现目标间的不一致和矛盾，Van Lamsweerde A[8]使用KAOS方法进行需求描述并设立目标级别用来解决异常。四是基于图描述的方法，此方法通过给定某些图的性质和语义关系，检测出需求描述间的不一致。Glinz M[9]提出使用场景模型和类模型相结合，通过建立交叉引用检测其中的不一致问题。

除了检测需求不一致问题，在处理需求冲突问题上也有很多研究，Lee K H[10]提出使用博弈论和基于目标的方法来分析需求之间权衡问题，目标模型用于分析利益相关者的目标和意图，博弈论的知识用来分析需求之间的权衡。Sadiq M[11]提出了一种基于模糊的方法在面向目标的需求启发过程中对需求优先级进行排序的方法，然后使用二叉树排序方法来获取需求的优先级列表，从而对发生冲突的需求提供消解策略。Suhaib M[12]认为在软件开发不同阶段，必须意识到不同类型的风险，需求冲突识别是软件工程的关键之一，其使用目标模型和矩阵的知识来量化子目标之间的冲突，为下一步的需求冲突消解做准备。Gulzar K[13]提出了一个新的框架，该框架侧重于使用模糊逻辑将可用性需求属性映射到用户的语言评估。框架优先考虑了冲突的可用性需求属性。框架旨在通过自动识别和解决可用性需求冲突的整个过程，帮助需求分析人员做出更好的决策。系统中的主要任务涉及确定每个属性的 权重，并考虑它们在不同的定量和定性评估标准中的重要性。Hassine J[14]提出了使用面向目标的需求语言GRL，集成了i*和NFR框架，提出对经验数据的统计分析，并利用统计学的方法来帮助检测和解决目标模型中的冲突。Zhang W等[15]认为现有的基于证据相似性的需求冲突研究计算复杂度大，难以满足系统实时性要求，提出使用于DEMATEL的新方法重新考虑每个证据的权重，由总关系矩阵得出相似度，然后计算重要性，最后基于Dempster的合并规则获得权重，此方法既能有效处理矛盾，又能降低计算复杂度。

关于需求不一致性和需求冲突的消解问题，国内也有许多相关研究，朱学峰、金枝[16]对于需求不一致的管理方面的工作做了比较系统的分析，总结目前需求不一致性处理的主要三种方法和需求重叠理论，提出了一种需求不一致和管理的框架。张建等[17]提出使用模型检验的方法进行一致性验证，将UML(Unified Modeling Language)的模型集合转化成时间自动机网络模型并使用模型检验工具进行一致性验证。周宇等[18]提出一种了一种从行为角度分析并采用时间自动机对软件演化过程中一致性的方法，将层次模型转化为若干并行时间自动机模型，并利用模型检验的方法和工具进行了验证。张璇等[19]借鉴了微观经济领域生产理论，提出了最优权衡代价决策方法，着重于实现如何选择最优方案实现需求冲突之间的最佳权衡。李瑞轩等[20]根据不同的策略目标给出了两种非一致冲突消解方法，最小代价方法和字典编辑最优方法，认为某个策略的加权冲突面较较大，则该策略与其余策略发生冲突的可能性较高。湛浩旻等[23]从需求的层次出发，提出使用解释结构和层次分析法相结合，用ISM(Interpretative Strucuural Model)方法进行分层处理，用APH(analytic hierchy process)方法进行优先级排序，当需求出现冲突时，通过需求的优先级来消除冲突。王守堰等[24]将博弈论中的纳什均衡策略应用于需求冲突当中，使用SCRI(strategy choosing tool for resolving inconsistency)工具和妥协谈判架构消除需求描述中的不一致需求。

1.3论文的研究内容及创新点 1.3.1 论文的主要研究内容 本论文主要研究如何发现需求描述中的不一致现象并解决这些不一致的需求冲突，主要研究内容如下：
（1）了解需求分析在需求工程的重要性，通过研究当前需求不一致方法，提出一种新的需求不一致研究方法，将需求不一致问题和需求冲突消解问题融入一个架构中，并建立统一的模型。

（2）本文在现有研究基础上对需求不一致问题进行研究。针对需求不一致的检测，本文提出对模型检验方法进行改进，提取使用自然语言描述的需求，利用相似性原理来解决需求不一致的定位问题，并制定出一套完整的模型转换方法供模型检验的工具所识别。

（3）针对从需求分析中或者后续由于增加新功能等导致的需求冲突问题，本文从需求关联度和代价权衡的角度考虑，综合考虑冲突的的类别和代价，提出一个完整的冲突消解框架来消除或者减少需求冲突。

（4）通过一个案例实际展示本文提出的基于模型检验的方法在需求工程中的应用。

1.3.2 论文的主要创新点 本文的主要创新点包括：
（1）提出一套完整的需求不一致的检测和消解方法，并以此为基础构建了一个新的建模分析框架。

（2）改进了基于模型检验的方法，解决了使用模型检验发现需求不一致问题不能定位的问题，为大规模需求分析减少工作量。

（3）对于需求冲突从单一因素消解到现在从其类别和代价权衡的方法方法考虑，更加适应时代软件发展的脚步。

1.4 本文的组织结构 本文由六个主要章节组成，每个章节的主要内容如下：
第一章：引言。本章主要阐述了本课题的研究背景和意义，主要介绍了需求一致性管理和需求冲突消解在国内外的研究发展现状以及目前存在的一些问题，并说明了本论文的主要研究内容和创新点。

第二章：研究框架建立。本章主要介绍了需求不一致问题和冲突消解问题，对当前的研究进行了总结，然后，在当前的研究基础之上提出了一个新的需求不一致与冲突消解研究方法，并结合该方法，给出本文研究需求不一致和需求冲突消解的研究框架。

第三章：基于模型检验的需求不一致研究。本章主要介绍了基于模型检验的需求不一致问题，总结模型检验的优缺点，提出需求子句相似度算法，用于解决模型检验的不足之处。总结并制定了由自然语言到自动机模型之间的转换规则，最后由模型检验的工具所验证。

第四章：需求冲突消解的研究与实现。针对于前文发现的需求不一致和需求冲突问题，本章给出相应的消解策略。在分析现有冲突消解的方法之后，首先对于需求冲突进行分类，针对于功能性需求采用基于关联度的方法进行消解，针对于非功能性需求采用基于经验和代价权衡的方法进行消解。

第五章：案例分析。对于本文提到的研究方法，本章通过一个实际电梯模型案例来说明本文提到的方法的可行性和有效性。

第六章：总结与展望。总结了本文所做的主要工作和主要成果。然后针对本文的研究内容和方法提出一些不足之处，并对未来要研究的工作做出展望。

第二章 框架研究建立 2.1 需求不一致问题概述 软件需求是以一种清晰、简明、一致且无二义性的方式对一个待开发系统中的各个方面进行描述的集合。软件需求分析的目的是获得清晰完整高质量的需求文档，为此，必须使用科学的方法和技术把用户在软件开发过程中提出的需求进行整理分析。此外，在软件需求中，一些软件设计过程中的约束、非功能性需求、在软件运行时和其他软件的关系也是需要分析的对象。

需求不一致问题是软件系统开发中的一个关键性问题，这个问题处理的好坏直接影响了软件规格说明书的质量，进而影响到软件产品的质量。需求不一致的来源有很多，从多视点的角度分析，不同的需求分析人员或利益相关者对待同一事物的描述是不尽相同的，这有可能导致不一致的产生。即使是同一个参与者对待同一事物的前后描述也有可能出现不一致现象。

2.1.1 需求不一致相关研究 关于需求不一致问题，已经有很多的研究，关于需求不一致的研究主要有以下几方面：
基于定理的方法：定理证明方法是形式化验证的主要方法方法之一，其主要思想是将需求描述形式化为逻辑表达式，然后利用定理证明中常用的方法如：归纳总结的方法、自然演绎法、基于表的方法等方法，找出需求描述中蕴含的矛盾，使用这些方法一旦检测出了矛盾就表示需求描述中出现了不一致现象。基于定理的方法的优点是可以严谨且具有一部分自动推理能力，近些年来像 NASA等使用基于定理的方法自动实现航天软件的正确性，其缺点就是基于定理证明的方法由于十分强调逻辑性的验证而导致过于需求描述过于形式化，难以被普通的需求分析这和利益相关者所掌握，且定理证明在效率上并不高，所以阻碍了技术本身的发展。

基于模型检验的方法：模型检验的方法是利用状态搜索的原理，是一种半形式化的方法。模型检验的基本思想是把需求等价为系统的状态变量，状态变量取值的不同表示系统处于不同的状态，然后设定性质规约，通过遍历的系统的状态，得出和预先设定的性质规约不一致的地方。基于模型检验方法的优点是其完全自动化并且速度快，且和基于定理的方法一样，都具有良定的检测过程。但是使用模型检验的方法来检测不一致也存在由于状态空间的急剧增长而影响本身这个方法效率和无法准确定位的问题，本文的第三章详细说明了如何改进这个方法。

基于目标的方法:基于目标的方法认为需求阶段的主要任务是确定系统想要实现的目标和实现目标所需要的约束条件。通过建立需求阶段目标所要的服务和约束的规格说明，将系统的实现看作是一个个目标不断分解、精化和抽象的关系。其中当两个目标的实现如果具有阻碍（thwarting）、破坏（break）、损害（hurt）、负向影响（some-）关系时，则认为出现了两个目的不一致问题，其中比较有代表性的工作时KAOS框架、NFR框架以及i*语言等。基于目标的方法优点是便于表达和处理冲突需求。

基于图描述的方法：基于图描述的方法也是一种半形式化方法，其原理是利用面向对象的图形形式和UML中的图相结合，其对于需求不一致检测的策略通常是根据转换的图自有的特性或语义，检测出其内部的不一致性。优点是图描述的方法便于表示和理解，缺点是其推导过程的逻辑性不足。

另外，对于某些特定的需求不一致的问题，还有采用人工检测的方法。

2.2 需求冲突消解问题概述 需求冲突消解是需求不一致问题的后续步骤，需求不一致实际上是需求分析中需求冲突的检测，而需求冲突消解则是提供消解的方法。需求冲突消解按照功能性分可以分成功能性需求冲突消解和非功能性需求冲突消解。按照模态形式可以分为静态消解和动态消解。按其处理方法可以分为直接去除法、修正冲突法和需求优先级划分法和基于协商的方法等。

2.2.1 需求冲突消解相关研究 关于需求冲突消解的处理方法，主要分为以下几个方面：
直接去除冲突：此种方法是冲突消解中最直接最快的方法，此种方法强调当在需求分析或者后续新功能增加时发现两个存在冲突的需求时，根据系统的一些特殊要求直接将某个需求删除。例如，在某个软件系统中，当强调某一项核心功能时，一旦遇到所有与核心功能不一致的需求直接删除掉此需求来保证没有冲突发生。但是此种方法在实际操作中并不常用，因为在不加任何比较和考虑的情况下直接删除一个需求，实际上是对系统整体功能的削弱。

修正冲突：此种方法的主要思想是当出现需求冲突时，对发生冲突的两个需求采用修正或改进的策略，通常会采用如弱化、分解、合并需求的方式来使两个冲突的需求减小冲突甚至是完全消解掉，此种方法是较为复杂的消解方式，因为在消解过程中既要保证消解的有效性，又要保证通过弱化、分解、合并的新的需求与原来的其他需求之间没有冲突。

基于优先级策略：此种方法强调对使用各种方法对需求设定优先级顺序，当需求冲突出现时，根据预先设定需求优先级，把优先级低的需求舍弃，优先先实现优先级高的需求，这样就可以消解掉冲突的需求。基于优先级策略是比较有效的方法，相比于直接删除和修正冲突的方法，此种方法在权衡利弊后做出决定。关于需求优先级还有很多的分类，例如：基于风险的需求优先级排序、基于需求可用性优先级排序和基于多属性决策的需求优先级排序等方法。此外，这种方法经常结合如APH（层次分析法），Delphi法（专家调查法）等方法来定性和定量考虑决策方法，从而避免了人为因素所带来的主观影响。但是这种方法通常缺乏优先级的协商、决策和调整机制，一般只能给出比较单一的优先级方案。

基于协商消解策略：基于协商的冲突消解的主要思想是通过分析利益相关者（stakehold）的之间的利益体现来消解不同的需求冲突。当需求出现不一致时，使用基于协商的消解策略，要对出现的冲突的两个需求进行识别，找出其需求后的利益相关者，然后矩阵、公式和逻辑表达式等对利益相关者进行协商处理，这种方式和修正冲突的方式最大的区别就是，基于协商的方法更加考虑需求背后的利益相关的需求，认为需求冲突的本质就是不同利益相关者对于需求的不同要求。

2.3 研究整体框架 本文在前人的研究基础上提出，一个新的研究框架，如图2.1所示，框架主要包含两部分，第一部分是需求不一致的研究，主要借鉴了模型检验的思想，在建模准备阶段使用自然语言对需求进行描述，便于理解，采用相似度算法为模型检验提供定位策略，并提供了一系列的转换规则，转换后的模型和属性规约一同交由模型检验验证，最终得出与属性规约一致或者不一致的结果。第二部分是需求冲突处理部分，在这部分中，通过对发现的需求进行分类，分成功能性需求和非功能性需求。对于功能性需求，提出使用需求关联度的方 法进行消解，把冲突中关联度小的需求进行舍弃或者精化。对于非功能性需求，可以继续分解为可度量策略和不可度量策略，对于不可度量策略，提出使用基于经验的方法进行消解，对于可度量策略 结合优先级策略和协商策略，改进了代价权衡策略。

2.4 小结 本节主要分析了现有需求不一致的研究方法和需求冲突消解的方法，建立了新的基于模型检验的需求不一致研究框架，并提出了相应的需求冲突消解方法，通过对不同冲突类型分别采用不同消解方法。除此之外，对于模型检验不能实现定位的问题，通过使用相似度的方法进行定位，完善基于模型检验的需求不一致的方法。

图2.1研究架构图 第三章 基于模型检验的需求不一致研究 上文第二章主要介绍了研究架构和主要方法，本章根据前文的框架，主要解决需求不一致确定的问题。本章首提出了使用自然语言和模型检验相结合的方法来确定需求不一致问题。提出使用需求子句相似度模型，根据这个模型将自然语言描述的需求进行相似度比较，确定可能存在需求不一致的地方，为模型检验提供定位策略。同时，从自然语言描述的需求中提取自动机模型，并提出一套模型转换方法，将自然语言描述的需求转换成模型检验工具能够识别的模型，然后将转换后的模型和提出的属性规约一起由模型检验的工具进行验证，得出与属性规约一致或者不一致的地方，并给相应的反例。

3.1 基于自然语言的需求描述与转换 3.1.1 需求子句相似度模型 在需求描述的过程中，表达能力较强的自然语言常常用于需求描述，使用自然语言描述需求可以使更多的需求相关者参与其中，从而使需求更加全面和完善。在然语言描述的需求中，不同参与者从不同视角描述的需求不可避免的存在不一致现象，Spanoudakis[23]认为两个需求描述元素之间存在重叠关系，这种重叠关系一共有四种，包含无重叠关系、完全重叠关系、包含性重叠关系和部分重叠关系，只有当重叠关系出现后三种的时候，才可能会导致需求描述的不一致性的现象发生，可以说需求重叠现象是出现需求不一致的根本原因。考虑到需求描述重叠的情况，本文提出使用相似度方法计算自然语言的需求描述，若两个自然语言的需求描述相似度越高说明重叠概率越大既存在需求不一致的概率越大。使用这种方法为下文的模型检验提供定位策略。

本节以自然语言需求子句为结点，构建了一种需求子句模型。如图3.1所示，使用句子相似度算法，表征句子之间的相似性。在处理过程中，本节将自然语言描述的需求划分为若个需求子句(sentence)，然后对需求子句进行分词处理,在这个过程中，统计每个需求子句中词语的词频(F)和词性(N),利用相似度算法计算出这些需求子句的相似度，把具有相似度需求子句放到一个组里。其中,词频(F)表示需求子句中某个词出现次数的统计量，其初始值为1，随着不断切词累加。词性(N),是一组枚举值，取值范围分别为名词（n）、动词（v）、形容词（adj）、副词（adv）、数量词（nq）、代词（pro）、介词（pre）、连接词（con）。为了解决部分词语不规范的问题，使用可替换同义词 (T)表示需求领域内对某些名词的通用规范用法。

图3.1需求子句相似度模型 算法3.1给出了需求子句相似度的计算过程，相应的算法伪代码表示如下：
算法3.1需求子句相似度算法 Input: Requirement Description ; Output: Similar Sentence ; begin: Requirement Description(DS) ∉∅；
//需求描述 Requirement Sentence(RS) ∈ ∅；
//需求子句为空 n* RS ← DS ; //将需求描述转换为n个需求子句 i=0,j=0;//设置变量i,j初始化 forall the Ai∈ RSi do n*Ai*Fi+n*Ai*N =RSi divided; //遍历所有子句，将子句进行分词处理，划分成词频和词性 newAi = n*Ai *Fi +n*Ai*N+T; //出现不规范词用专业词替换 foralltheFiinnewAndo //重复遍历每一个分词处理结果 j=i；

forallthe Fj in newAn/2 do //任意两个之间做比较 j=i; if(SimFreq(Fj,newAn/2)>0.5) //相似度大于0.5 then add Fj∪newAn/2 join Similar Sentence[ ]//相似的放在一组 n++; //继续循环 i++; //继续循环 end; 需求描述里的关键词信息能够直观反应关键词在文本中的重要程度[24]，当某个需求关键词在文档中出现的次数越多，说明这个关键词在整个文档中占的比例越大，所占的权重越高。为了求两个需求子句之间的相似度，本文借鉴于传统的VSM[25]计算方法，基于向量空间模型的算法，使用两个向量的夹角表示出两个向量之间的相似度。在此过程中，把每个词看成一个维度，而词的频率看成其值，即向量，这样两个需求子句的相似度就是每个句子的词及频率构成的空间。其计算过程如公式3-(1)所示 公式3-(1) SimFreq=F,S=F·SF×S =i=1n(xi×yi )i=1nxi2×i=1nyi2 通过公式3-(1)来计算两个需求子句之间的相似度, 其中F和S是分别是两个需求子句向量形式，xi和yi是向量的值。

本文首先根据上文提到的需求子句进行分词处理，然后进行词频计算并形成特征向量，这样可以将两个需求子句这种非结构化数据抽象为向量表现形式, 之后便可以将自然语言表述的需求问题转换成数学上的向量夹角问题，同时需求关键词词频的数量在一定程度上能够反映重要程度，当需求描述文本规模比较大时，使用此方法可以有效且快速的找出需求相似的地方，为解决需求不一致提供定位策略。示例过 程如下所示：
假设有两个需求描述子句如表3.1所示。

表3.1需求相似度计算示例 编号 自然语言描述 1 乘客按下向上按钮，电梯响应请求，向上运行。

2 乘客按下向下按钮，电梯响应请求，向下运行。

以上需求子句经过分词处理得：
需求子句1:“乘客 按下 向上 按钮 电梯 响应 请求 向上运行” 需求子句2:“乘客 按下 向下 按钮 电梯 响应 请求 向下运行” 获得向量集 “乘客 按下 向上 向下 按钮电梯 响应 请求 向上运行 向下运行” 对于需求子句A进行处理的结果是: 乘客(1)按下(1)向上(1)向下(0)按钮(1)电梯(1)响应(1)请求(1)向上运行(1)向下运行(0) 对于需求子句B进行处理的结果是: 乘客(1)按下(1)向上(0)向上(1)按钮(1)电梯(1)响应(1)请求(1)向上运行(0)向上运行(1)。

经过词频计算得A需求子句的特征向量{1,1,1,0,1,1,1,1,1,0}，B需求子句的特征向量 {1,1,0,1,1,1,1,1,0,1}。

根据公式3-1计算得两个需求子句的相似度 SimFreq=F,S=F×SF×S =23 其中: F=1,1,1,0,1,1,1,1,1,0,S={1,1,0,1,1,1,1,1,0,1} F×S=6 F=12+12+12+02+12+12+12+12+12+02=4 S=12+12+02+12+12+12+12+12+02+12=4 其计算结果为2/3，说明在需求描述中两个需求子句比较相似，根据需求重叠理论，需求越相似的地方存在不一致的概率越大,所以首先定位到这两句需求描述的位置，以这两句为基础结合上下文进行建模分析。

3.1.2 自动机模型 自动机是有限状态机(FSM)的数学模型, 是表示有限个状态以及在这些状态之间的转移和动作等行为的模型。有限状态机是一个五元组：（Σ,Q,Δ,q0,F）
其中：
Σ是一个有限字母表。

Q是一个有限状态集合。

Δ⊆Q×Σ→Q代表变迁关系。

q0⊆Q是起始状态。

F⊆Q终止状态的集合。

图3.2自动机模型 自动机可以用于并发系统和交互式系统建模。一个简单的自动机模型如图3.2所示，q0表示系统的起始状态，q2和q3属于终止状态F，q1是过程状态，它们都属于状态集合Q，其余为状态变迁。状态Q和字母表Σ都可以表示待建模系统状态的集合。

3.1.3从自然语言提取到自动机模型 本节中，将需求定义为一组由动作序列控制的状态变迁关系[26]，以此刻画自动机模型,将具有分解规范的自然语言指定为由事件(Event)、状态(State)以及动作列表(Action)组成的结构。这种类型的规范结构描述了一个由动作和事件驱动的状态改变结构。其中，Event是指导致系统表现出可预测行为的动作或过程。State表示某时刻系统的某个行为。Action表示人或系统的操作列表，可能会导致状态的改变。一个简单的状态变迁图如图3.3所示。

图3.3一个Event事件的状态变迁图 本节结合此方法和BDL方法Error! Reference source not found.对模型进行改进，改进后的表述使用电梯模型描述此行为，如表2所示。

表2 具有分解规范的自然语言分解过程 FSM中的元素 对于元素 分类 提取 来源 Event Subject 电梯 n. Behavior 空闲、上升 v. adv. q0,Q,F State State 待载、上升 v. adv. Agent 乘客 n． Δ,Σ Action Activity 按下 v. Object 按钮 n． 使用以上表格分解规范时，需要施加规则。其中Action中的Agent表示代理，可以参与到一个或多个动作当中，是与系统交互的人或系统，是行为的执行者。Activity是人或者系统执行的操作，可能会导致状态的改变，是行为本身。Object是受到原子动作中代理和资源作用影响的人或其他系统，是行为的被执行者。在电梯模型中，由于Action而导致整个系统的改变，开始时电梯在一楼，为空闲状态，乘客进入电梯后,电梯由空闲变为待载，等待上行的指令。当乘客按下按钮时，乘客作为代理操纵了系统，导致了系统状态的改变，电梯由待载状态变为上升状态。根据上文提到的表格将具有分解规范的自然语言描述的需求分解成自动机模型如图3.4所示 图3.4电梯空闲事件的自动机模型 上图描述了由自然语言过渡到自动机模型的一个例子，从图中可以看出，由于整个的 Action行为才导致系统状态的变迁，这符合BDL中描述的行为执行者依照软件功能对被执行者实施操作的过程。

3.2 基于模型检验的需求不一致 模型检测是一种基于状态搜索的形式化验证技术，采用自动化技术遍历状态空间，检查所遍历的状态空间是否满足提出的性质规约，如果发现了和预期性质不一致的地方，则会自动定位到错误的位置。模型检测这项技术已经被成功应用于计算机硬件，通信协议、控制系统和安全认证灯方面。模型检验方法的优点，模型检验方法因为是自动化方法，所以检测过程比较快，由提供的属性规约和模型检测工具，自动得出与属性规约不一致的地方，也就是通常所说的“反例”，并说明为什么不满足，方便查找和检测需求分析和设计中的缺陷。

模型检验最早是由Clarke和Emerson以及Quielle和Sikakis在针对时态逻辑实际验证算法时提出。目前在系统的安全性和一致性方面应用很广[27]模型检验是一种自动验证系统模型是否具有特定性质方法，简单来说就是先把系统建模为有限状态转移系统，后利用时态逻辑描述待验证的规范，对整个系统的行为空间进行自动化的遍历搜索，与定理证明按照一步步展开严格证明推导不同，模型检验具有自动化和高效化的特点。

模型检测一般包含三个步骤:系统建模、性质描述、性质验证。

系统建模（modeling）：模型检验的方法是形式化的方法，因此首先需要将待测系统进行形式化，即从待测系统中提取出一个Kripke结构或者是一个有穷状态变迁系统，并在这个结构中增加初始状态集和终止状态集。通常需要在建模的时候利用抽象的技术来进行剪枝，来减少模型状态爆炸问题。

性质描述（specification）：通常建立一个系统，总是期望该系统满足一定的性质，如安全性、一致性等。性质描述就是对于已经建立的模型通常采用模态逻辑或时态逻辑公式或自动机的形式来表示，这些所有的性质都可以称之为属性规约。

性质验证（verification）：性质验证的主要工作就是里利用现有的模型检验工具和属性规约自动验证，得到一个肯定或者否定的结果，肯定表示属性规约符合开始的预期，说明此性质得到验证。否定表示属性规约不符合预期，得出“反例”。并且会产生一个错误路径，帮助分析者和设计者跟踪发生源。

在模型检验中，把系统的状态变换等价为变量值的变化，变量值的改变体现了状态的迁移，利用状态间的约束关系和状态转移的关联关系构成自动机模型或状态图[29]模型检验中使用上文的自动机模型可以将系统和待检测的性质用同一种方式来表示。其检验过程如下图3.5所示。

本文将需求描述的系统模型的自动机图，转化为一个模型检验的问题，即将自然语言描述的需求问题，转换模型检验中的“状态不可达”，“不存在此条路径”等类似性质进行验证[30]。

图3.5模型检验过程 通过建立被测系统的状态行为模型，并用CTL时态逻辑描述系统待验证的性质，经由模型检验工具NuSMV检测，最终得出一条反例。反例的出现首先表明性质规约验证了模型，其次反例的出现可以加大对模型的理解，发现模型的不足。基于此，增加对模型的验证部分，包括可达性，前向一致性，陷阱性质的验证。其中，可达性的表述为在一次状态变换中，总是至少存在一条路径可以到达目标状态。前向一致性的表述为如果某个状态S1出现，那么该系统模型在后续变换中一定能够出现可预见的状态S2。例如，事件S1表示电梯系统启动，事件S2表示乘客按下上行按钮，事件S3表示电梯到达目标楼层。则事件S1和事件S2满足前向一致性。陷阱性质的描述为对某一性质进行取反操作，由模型检验的工具进行检测。通过检测以上性质可以得出和预期不一致的地方，并通过产生的反例帮助构建更为完整的需求模型。

3.2.1 模型检验及相关定义 定义：Kripke结构：令AP为原子命题集合，则AP上的Kripke结构M是一个三元组M=(S,R,L)其中，S是状态的有限集合，R是完全变迁关系，L是标记函数，它标记在该状态下为真的原子命题集合。

Kripke结构有向图中，用圆圈表示可能的事件，有向弧线表示可能事件的关 系，标记函数在圆圈内。如图3.6所示。

图3.6 一个Kripke结构 CTL*是一种离散、分支时间、命题时态逻辑，将系统的状态变化的所有可能性表示为树状结构。CTL*公式主要由原子命题、布尔运算符、时态算子和路径量词构成。CTL*公式主要由两种类型：状态公式和路径公式。路径量词的作用是表 述计算树逻辑的结构，由A和E两种构成, A表示从当前开始在未来的所有路径符合某一性质。E表示从当前开始在未来至少 有一条路径符合性质。

时态算子有5个基本的运算符，直观上的意义如下：
X(“Next”)说明从某状态起始路径的第二个状态开始，性质满足。

F(“Finally”)刻画从路径中的某个状态开始，最终性质满足。

G(“Global”)说明性质在路径上的每个状态都满足。

U(“Until”)表示在此状态之前路径上所有状态第一性质满足。

R(“Release”)表示从当前状态开始到满足第一个性质的状态结束，第二个性质一 直保持成立。

总之，根据语法规则，CTL*是状态公式的集合，它是描述反应式系统在状态之间转换序列的形式化方法。

定义2：计算树逻辑（computation tree logic）CTL是CTL*的子逻辑，主要限制是时态算子X、F、G、U、R必须在其前面加上路径量词。

定义3线性时态逻辑LTL：LTL也是CTL*的一个子逻辑。它的公式具有形式Af，其中 f是路径公式，并且包含在f里的子状态公式仅仅是原子命题。

其区别如下：
图 3.7状态迁移系统 CTL和LTL是两个不可比系统。例如考虑图3.7的状态迁移系统T：
显然T⊨FGp；
考虑路径ppppppp…,在该路径的任意节点，AGp均不成立，因此T⊭AFAGp。两个性质之所以“不一样”，是因为存在状态转移使得其中一个公式 成立而另一个不成立，即它们描述的并非同一性质。CTL*逻辑是CTL和LTL的组合，这些逻辑在模型检验中是最经常运用的。

3.2.2模型检验实现 本文以一个简单的例子来说明模型检验算法。例如：房间加热器可能处于如下的四种状态中的任何一个：Idle——空闲状态；
End——结束使用；
Heat——开始加热，达到某个温度；
Warning——系统警告。图3.8给出了房间加热器Kripke结构。为清楚起见，每个状态都用在该状态为真的原子命题和在该状态为假的原子命题的否定形式标记出来，带箭头的弧标记表示了引起状态变迁的动作名称。

根据上图描述的结构，提出一个性质规约使用CTL公式描述：AG(Idle→AFIdle)，该公式等价于EF(IdleEGHeat)。从满足原子公式的状态集合开始标记，进而是复杂的子公式。令S(g)表示子公式g标记的所有状态集合。

S(Idle)={2,5,6,7} S(Idle)={1,2,3,5,6} 为了计算S(EGIdle)首选得出S’=S(Idle)中的非平凡强联通分量的集合为SCC={{1,2,3,5}}，后续的步骤用来求由EGHeat标记的状态集合，即各SCC中所有元素的并集，初始时 T={1,2,3,5}。因为S’中再没有其他状态可以沿着S’中的一条路径达到T中的任意一个状态。因此，计算中止于 S(EGIdle)={1,2,3,5} 接下来计算S(IdleEGIdle)={2,5} 在计算S(EF(IdleEGIdle))时，首先令T=S(Idle EGIdle)。接着，使用变迁关系的逆关系来标记满足公式的所有状态，可以得到 S(EF(IdleEGIdle)={1,2,3,4,5,6,7} 最后可以得到 S(EF(IdleEG Idle))= 因为结果集合中没有包含初始状态1，所以可以得出结论：这个用Kripke结构描述的系统不满足给定的性质规约。

图3.8房间加热器的Kripke结构 3.2.3 模型转换 采用模型检验方法需要对被测系统进行建模分析，用时序逻辑描述系统的结构和性质，利用模型内部的状态迁移关系来验证整个模型内部某些特定性质是否正确。本文用模型检验中的SMV语言描述描述待测系统，用CTL时态逻辑描述系统 性质。对模型内部中系统状态的可达性进行分析 将上文提到的自动机图提取状态元素转换成SMV模型，以供模型检验的工具所识别。SMV模型包含变量声明模块VAR和IVAR，关键字定义模块MOUDE；

使用ASSIGN模块定义系统的初始状态，使用INIT定义系统初始状态的变量 值。其对应转换规则如表3.2所示。

表3.2 自动机图中元素与SMV的对应关系 图中元素 SMV模型 说明 State VAR，IVAR 变量声明，所有状态的集合 （源状态、初始状态 、目标状态）
ASSIGN(init) 定义约束的集合 Event Next 表示状态的改名，当前状态收到主题或代理的影响，准备迁移到一下状态 Action case…esac 系统状态变量受到触发引起的确定的下一个状态。

按照表3.2描述，可以将上文中的自动机图用SMV的语法表达出来。如下所示: MOUDULE main VAR state：{IDLE,UP,DOWN} button_F1:boolean ASSIGN: init(state):IDLE; init(button_F1):false; next(state):case state:IDLE&button_F1:UP esac; 可以看出，提取出图中元素后按照对应关系可以将上文提到的自动机模型逐步转换成能被模型检验工具所识别的SMV模型。

3.2.4反例及其作用 本节使用经典的山羊过河问题来说明模型检验的反例的应用。问题描述如下：一个人带着狼、山羊和白菜在一条河的左岸，有一条船，大小正好能装下这个人和其它三者之一，人和他的随行物都要带过岸，但他每次只能带一样东西摆渡过河。

如人将狼和羊留在同一岸，无人照顾，那么狼会把羊吃掉。同样，如羊和白菜在同一岸，无人照顾，那么羊会吃了白菜。其中MGCW-Empty表示初始状态。“—”左边的符号表示对应的符号在左岸。“—”右边的服务表述对应的符号在右岸。

M表示人，G表示羊goat,C表示白菜Cabbage,W表示狼wolf. 箭头表示表示每次在船上运输的物品的种类。详细描述参见附录1 图3.9 农夫过河问题有限状态机 安全过河的条件是 TLSPEC E [( ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))] 图3.10 模型检验的正例验证 验证条件如图3.10所示，显示是true，说明提出安全过河的性质规约对于建立的模型来说是正确的，因为模型检验工具NuSMV只会提供不符合性质的例子，也就是反例，因此为了得到一个反例，可以对安全过河的条件取反， TLSPEC ！E [( ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))] 表示不存在这样一条路径，然后交由模型检验工具NuSMV验证，验证结果如图3.11所示，结果显示给出的性质规约为false，并且给出了一条反例，反例的出现说明了对于出现了与属性规约不一致的地方，并且直接给出了一条路径。

图3.11 模型检验反例验证 3.3 小结 本节以模型检验为主要研究内容，通过自然语言的相似度算法为模型检验提供定位策略，并从自然语言的描述中提取出自动机模型进而由模型转换方法变成模型检验工具能够识别的语言，最后，通过样例说明了模型检验的工作原理并说明了模型检验反例的由来及作用。

第四章 需求冲突消解的研究与实现 上一章中使用模型检验与自然语言相结合的方法研究了需求不一致问题，当在需求分析过程或者由于系统升级增加新功能等而导致了需求不一致问题的发生，则应该消除掉发生的需求不一致，也就是本章的需求冲突消解问题。本章首先对于冲突的需求进行分类，分解成功能性需求和非功能性需求，针对与两种不同类型的需求冲突，采用不同的消解方式，对于功能性需求，采用关联度的方法进行消解，对于非功能性需求，借鉴经济学中的生产理论和成本分析法提出代价权衡策略，综合考虑非功能需求从而达到消解冲突的目的。

4.1 概述 针对与大型软件和复杂系统的开发，为了获取更加全面的需求，防止需求信息的遗漏，往往需要从不同视点不同利益相关者（stakeholder）的角度进行考虑分析，这其中由于来自不同视点，不同利益相关者的需求不可避免的存在冲突，需求冲突的消解成为需求分析中无法回避的一个重要问题。即使用何种方法来消解掉需求描述中的冲突。

对于冲突消解问题一般从需求的优先级和权重两个角度分析。需求优先级和权重。需求优先级用于解决需求冲突问题时，一般结合一些具体的方法，比如，层次分析法（Theanalytichierarchy process）简称AHP，其基本思路是建立系统的层次结构模型，将有关某项需求的各个因素按照不同属性自上而下地分解成目标层、指标层和方案层，然后通过构造对比矩阵来判断矩阵中某个元素的标度，分别计算单次或组合的权向量来决定出哪些元素的优先级高，哪些元素的优先级低。此外，还有一些对AHP方法进行组合做改进的方法，基于ISM（InterpretativeStructuralModelMothod）与AHP方法相结合，基于SAHP方法，基于Topsis（Technique for Order Preference by Similarity to an Ideal Solution ）与AHP结合的方法等。还有一类方法确定优先级的方法是KNAO模型，KANO模型将用户需求分为基本型、期望型、兴奋型、无差异型和反向型以分析用户需求对用户满意度的影响，体现了用户需求满足程度和用户满意之间的非线性关系。但是大部分的优先级方法都比较单一缺乏动态调整决策机制。另一种解决冲突的方法是确定每个需求的权重大小，权重是用来衡量总体中单位标志值在总体中作用大小的数值，是表示某一项指标在系统中的重要程度，它表示在在其他指标项不变的情况下，这一指标项的变化对结果的影响。权重赋值的方法常见有三类：主观赋权法，客观赋权法，组合赋权法。其中主观赋权法，通常有专家调查法（Delphi法），层次分析法（AHP 法），二项系数法。客观赋权法，主要包括主成分分析法、熵值法、多目标规划法、离差及方差法等。主客观赋权法是结合主观客观思想主客观赋权法包括折衷系数综合权重法、线性加权单目标最优化方法、熵系数综合集成法。另外，对于权值确定，还有使用多属性决策的方法，例如DEMATEL方法、C2R方法等，这些多属性决策的方法通常结合需求优先级来综合考虑权重问题。

冲突从stakeholder角度分析可以分为业务冲突，目标冲突，情感冲突。本节指的是目标类冲突，目标类冲突指的是系统的需求，一般包含功能性需求和非功功能性需求。其中，功能性需求求规定了开发人员必须在产品中实现的软件功能，用户利用这些功能来完成任务，满足业务需求，它是系统中必须具备的功能。软件非功能需求也称为质量需求或者质量属性,实际上是软件的属性或者是功能需求的约束。非功能需求为软件产品为满足用户业务需求而必须具有且除功能性需求以外的特性，影响着产品是否能够持续并高效的提供服务。非功能性需求和非功能性需求都很重要，功能性需求描述系统想要完成的功能或任务而非功能性需求通常描述软件需要满足的某些属性的程度，对于非功能需求难以用量化的手段来表示，其满足需要受到时间，成本和风险等各种因素的影响。

4.2 功能性需求冲突消解 4.2.1 需求关联性与一致化程度 定义：需求关联性：基于本文的自然语言和模型划分，按照划分后的需求元素之间是否有联系的情况，来判断两个或者多个需求元素之间是否有关联性。

定义：需求关联度：需求关联度L是针对于需求原集A和需求冲突集B的一个比例关系，如公式1所示 Li=A∩BiA。

公式4-(1) 其中：A是需求原集，它是由本文提出自然语言分解后的需求集 B是冲突集，它来自两部分，一部分是原需求描述中冲突的部分，另一部分是由于升级或者增加新功能导致与原需求冲突的部分。

Bi是冲突集中的具体的某一个冲突，Bi⊂B 图4.1需求关联度 4.2.2 基于需求关联度冲突消解 针对于功能性需求之间的冲突，本节提出使用基于需求关联度的消解方法，针对于复杂系统建模时，其消解流程可以概括如下：
（1）结合第三章的划分成需求子句提取需求原集A。

（2）根据模型检验的结果提取出两个具有冲突的集Bi和Bj。

（3）根据公式4-(1)计算出冲突集Bi和Bj和需求原集A的关联度。

（4）分析并比较两个冲突的需求元素之间的关联度的大小，将关联度更低的 需求进行精化或者舍弃。

在功能性需求冲突消解中，需求关联度是一个很重要的判断依据，相比于直接根据需求优先级的方法，需求关联度可以综合考虑需求元素之间的联系，一个系统 的状态图分解后如图4.2所示。

在此图中，所有的需求都被分解成若干个子需求，从子需求刻画成状态模式，可以看出对于一个确定的系统来说，其状态变迁关系应该是唯一确定的。现在假设有个冲突的需求集B，当其加入到需求原集A中，其新的需求q10与原集中q3冲突，会引起系统的不确定等问题。提取出q3需求，如图4.3所示。冲突集B与需求原集存在关联性，其示意图如4.4所示，可以看出在冲突集B中包含的元素中与需求原集有重叠，将重叠部分取出进行对比可以发现，q3这个需求与需求原 集有4个不同的关联，q10这个需求与原集有3个关联，还有一个无关关联。

图4.2 一个系统需求分解 根据本节式4-(1)可以得出q3这个需求的关联度是 Lq3=A∩BiA=410=40%,而q10这个需求的关联度是Lq3=A∩BiA=310=30%。根据需求关联度理论，应该对q10这个需求进行舍弃或者精化。

图4.3 冲突集提取 图4.4新冲突集 4.3非功能性需求消解 4.3.1 代价权衡分析 本文针对于非功能需求难以量化的问题，借鉴经济学理论，改进非功能性权衡代价分析方法，改进的目的是:保证两个非功能需求发生冲突时，总是让代价最小损失，从而整体上保证软件的质量。软件非功能需求的冲突本质是利益相关者因策略执行而不可避免引入的。如果策略不执行，则不会导致冲突，但是在很多情况下，为了提升某些非功能性需求，必须执行特定策略。例如，很多软件会把安全性和响应时间作为非功能需求需要考虑的要素，在这个情景中，由于考虑到安全性， 强制实施密码策略，增加密码的复杂度和认证程序，在此过程中，由于复杂度增加，势必导致响应时间增加。也就是说针对于这两个非功能性需求，提升安全性的同时必然会损害到响应时间，或者说，为了提高响应时间的代价是降低系统的安全性。所以，必须找到非功能需求之间的最佳权衡点，让系统的整体代价损失最小。

本文借鉴经济学中代价权衡理论，将经济学中的生产理论与需求工程相结合，综合权衡非功能性代价，让代价损失最小。为了更好的表达非功能需求，本文讲非功能需求分为两类，一类是可度量的策略，另一类是不可度量的策略。

4.3.2 不可度量策略 不可度量的策略通常不能用现有的量化方式对非功能需求进行量化处理，与就是说难以采用数学的方法对非功能需求进行代价权衡。例如，在Stacey Matrx模型 中，如图4.5所示。

图4.5 STACEY矩阵模型 当问题没有确定时，因果关系不明显，垂直（Y）轴是团队，团队和组织之间就问题或决策达成一致的程度。在频谱的一端，如果在这个问题上存在高度的确定性和一致性，那么决策就很容易，这个领域被称为（理性或简单），传统方法（瀑布）和方法是最有效的。在另一个范围内，没有就该问题达成一致意见，也没有确定因果关系。在这个地区，计划通常是慷慨的，这是一个混乱和无政府状态盛行的地区。这是极端不稳定和稳定性不可逆转的极端，应该避免混沌区域。在频谱的两个极端之间存在称为复杂区的大区域。这里的传统方法并不是情感因为复杂区域中的系统是不可预测的。在此区域，既不能提前指定产品详细信息，也不能在准确度方面就这些详细信息达成一致。这些条件需要用户和开发人员之间的协作环境。最佳使用方法是敏捷，因为它需要高度的创造力和创新才能产生解决方案。在敏捷开发中，软件项目的构建被切分成多个子项目，各个子项目的成果都经过测试，具备集成和运行的特征。简单地来说，敏捷开发并不追求前期完美的设计、完美编码，而是力求在很短的周期内开发出产品的核心功能，尽早发布出可用的版本。然后在后续的生产周期内，按照新需求不断迭代升级，完善产品。由于敏捷开发中强调人的作用，从最小的单一功能入手，因此在遇到需求冲突时很难 权衡量化，针对于不可度量的策略，使用基于经验的方法进行冲突消解。其基于经验的需求冲突消解如下：
（1）从每个小型团队开始，发挥人的作用，以人为最小单位组建。

（2）发现冲突时，先进行内部讨论，如果经过人员的内部讨论解决了冲突则把此案例放到策略库中以备后用。

（3）如果经过内部讨论没有解决这个问题，则要进入调解程序， 调解程序的主要目的是使用人员的开发经验进行决策，解决之后的策略放到策略库中。

4.3.3 可度量策略 对于可度量非功能需求冲突，采用经济学中的生产理论对非功能需求进行权衡分析，例如，可信软件中认为，如果一个软件的行为总是与预期相一致，则称为可信，一个可信软件的应该是软件及其结果是可以预期的。所以对于能够预期的解决采取可度量的策略。

定义1：策略代价Ps：一个策略S的代价Ps是实施策略S引发非功能需求集合R的策略代价P和其成本PM的一个函数关系，其中， （1）S是为了满足非功能需求必须实施的某个策略 （2）R是策略S引发冲突的非功能需求集合，∀r∈R 是一个具体的非功能需求 （3）PM是使用策略S时产生的工作量即成本代价。

定义2：成本代价PM：PM是在策略S下而产生的成本。其公式如下：
PM=A×（SIZE）E×i=1nEMi(i=1,2,3…17) 其中：
（1）PM为总工作量，即使用策略S时的成本; （2）A为生产率常数，在COCOMOⅡ中，A通常取值为2.98 （3）SIZE为估算的软件功能单元的代码行数， （4）E为指数因子，反应了项目的规模经济性；

（5）EMi为成本驱动因子，用于获取影响完成项目所需工作量的软件开发特征。一个成本驱动因子是一个模型系数。在COCOMOⅡ中定义了17个成本驱动因子。

其中，指数因子E计算公式如下：
E=0.91+0.01j=15SFj 上式中，j=1,2,3…5;指数因子E体现了5个比例因子SFj的作用，说明了不同规模的软件项目具有相对的规模经济和不经济性；
SFj 为比例因子，是项目工作量指数变化或生产率变化的重要成因，每个规模因子都有一个登记变动范围，从“很低”到“极高”。

在经济学的生产理论中，生产函数Q是劳动L和资本K的一个函数关系， Q=f(L,K),当使用生产理论来描述两个非功能需求的冲突时，L和K为两个冲突要素r1和r2，Q为产生的策略代价度量P，然后以度量值构造代价线。如图4.3所示。PM是两个冲突要素中以其中一个为自变量的产生的成本代价线，如图4.4所 示。n1和n2分别指因策略S的实施而产生的需要权衡的非功能需求冲突。当策略S被实施时，r1的度量值为x1时，在r2对应的度量值为y1；
在r1取x2时，在r2取y2。依次类推，产生了策略S的策略代价线P。对于成本代价线PM，当以n1为自变量时，r1这个非功能需求取值x1确定时产生的成本代价y1，r1这个非功能需求取值x2时确定成本代价y2，以此类推，产生了策略成本代价曲线PM。策略代价线P上有xi和yi决定的的代价点描述的是因策略S实施而在非功能需求r1和r2之间反应的权衡关系而策略成本线PM，反应了因策略S实施在不同阶段的成本代价。此权衡关系可以视为r1和r2之间的弹性代替关系。由图4.x可见，如果r1要取最高点x4，则n2只能取最低点y4，与此类似，当对r1降低要求时取x3时，n2就可以达到比y4高的y3，即r1和r2之间视为此消彼长的替代关系，这个关系描述了非功能需求间相互替代的代价。成本代价线如图x所示，当需求r1取值x1时，其产生了一个成本y1,当需求r1取值x2时，其产生了一个成本y2。

图4.3策略代价 图4.4成本代价 最优权衡代价决策，由上图4.3可以看出，由于某个策略的实施，一个非功能性需求的增强会导致另一个非功能需求的降低或者减弱，这是一个动态的过程，基于这个思想，我们需要对非功能需求增加必要约束，这样就可以找到利益相关者的最优权衡代价。

如图4.3所示，对于策略代价，增加两个约束条件一个是利益相关者对于非功能需求的优先级约束，另一个便是对于某个非功能需求的最低约束基线。优先级约束线是利益相关者对非功能需求之间冲突的权衡关系。如图4.5所示，可以用若干条直线来表示非功能需求 的优先级约束,斜率大的r1/r2说明对于这两个非功能需求，r1的优先级比r2高，利益相关者更需要r1。效率小的R1/R2说明对于这两个非功能需求，R1的优先级比R2低，利益相关者更需要R2。最低约束基线是利益相关者对于某项非功能需求的最低限制，如图4.x中的阴影部分。在很多非功能需求中，都有最低限制，比如在一个内容分享网站中，显示的内容的量和响应时间就是一对冲突的量，一项调查显示，用户最多愿意等待6秒，超过6秒就会失去耐心。所以，对一个这样一个系统来说，其响应时间这个非功能需求的最低约束基线就是6秒。同样，对于内容量也有最低的约束。

基于以上的两个约束条件，可以得出在约束条件下最优的策略代价，如图4.6阴影部分所示。R1-min表示非功能需求R1的最低约束基线，R2-min表示非功能需求R2的最低约束基线。(R1/R2)1和(R1/R2)2分别表示非功能需求R1和R2两种不同的优先级，那么对于两个非功能需求R1和R2来说，首先排除了不在此范围之内的策略X1。剩余两个策略X2和X3。其最优策略需要继续引入成本代价线PM，如图4.7所示，在此图中可以看出，根据前文R1与PM的关系，可以把成本代价线和策略代价线融合在一个坐标系中，可以看出在成本代价线与阴影部分有交点PM1，表示需求R1的成本变化关系，则需要考虑X2和X3对应的Y2和Y3与PM1的绝对距离，保留距离成本代价曲线点PM1近的策略X3。至此，对于非功能需求R1和R2，其代价权衡策略已经给出。

图4.5有约束的策略 图4.6基于约束的策略代价 图4.7最优权衡代价 4.4 小结 本节建立在发现需求冲突的基础上，对不同的需求冲突进行分类，对于功能性需求采用需求关联度的方法进行消解，对用非功能性需求采用代价权衡策略进行消解，最终实现需求的一致性。

第五章 案例分析 由于完整的系统模型庞大而复杂，本文通过精简电梯模型[31]Error! Reference source not found.，选取电梯模型对上述研究方法进行验证。

5.1电梯模型的描述与建模 电梯的功能分为上行、下行、报警、显示、开/关门、电话机报警等。该模型的部分自然语言描述如下：
上行：电梯初态停在一楼。当乘客按下上行按钮后，电梯响应乘客的请求，向上运行。到达乘客所在楼层后，打开电梯门，乘客进入电梯，电梯检测乘客重量是否超标。如果超重就报警，否则就关闭电梯门。然后乘客在电梯内按下目标楼层。电梯系统判断目标楼层大于当前楼层，电梯向上运行。到达后乘客打开电梯门，乘客离开。电梯停在该楼层，并重新处于静止状态。

下行：当乘客按下下行按钮后，电梯响应乘客的请求，向下运行。到达乘客所在楼层后，打开电梯门，乘客进入电梯，电梯检测乘客重量是否超标。如果超重就报警，否则就关闭电梯门。然后乘客在电梯内按下目标楼层。电梯系统判定目标楼层小于当前楼层，电梯向下运行，到达后乘客打开电梯门，乘客离开。电梯停在该楼层，并重新处于静止状态。

报警：乘客在电梯内按下报警按钮，或者电梯出现故障紧急停止后，报警。

显示：显示面板会一直显示电梯的状态(运行状态，当前所在楼层)；
如果发生故障或者乘客按下报警按钮，显示面板显示为“不可用” 开/关门：乘客在电梯内/外按下开/关门的按钮后，电梯响应，打开或关闭电梯门。

对以上自然语言使用2.1节中的相似度算法进行分析，得到描述上行和下行需求描述的相似度约为0.95，说明两个需求描述存在重叠的地方，所以定位到这两个需求描述的位置以此位置开始进行建模分析，避免遇到大规模的需求描述无法快速找到潜在不一致需求的情况。发现具有相似性需求描述后，根据 3.1.2节中的分解规范提取自动机模型，其分解过程如表5.1所示。

表5.1 分词提取后的结果 项 需求描述 根据分解规范提取 对应元素 #1 电梯最初停在一楼 停（电梯，一楼）
State #2 乘客按下上行按钮 按下（乘客，按钮）
Action #3 电梯响应乘客请求，向上运行 向上（电梯，乘客，）
State #4 乘客到达楼层，乘客进入电梯， 到达，进入（乘客，楼层，电梯）
Action #5 电梯检测重量是否超标 检测（电梯，超标）
Action #6 到达后乘客打开电梯门，乘客离开 打开，离开（乘客，电梯门）
Action #7 乘客按下下行按钮 按下（乘客，按钮）
Action #8 电梯响应乘客请求，向下运行 向下（电梯，乘客）
State #9 … … … … … … … 根据表格提示结合上下文补充必要的节点可以生成自动机模型，为了便于观察，转换成自动机形式，如图5.2所示。根据上文表3.2的方法结合图3.4，可以简单生成一个电梯系统的SMV模型，该模型表述如下所示：（由于篇幅有限，只选取部分关键代码）。

图5.2 电梯模型的一个模型描述 MODULE main VAR state:{Up,Down,Hold,Idle,Waiting,Warning,Stop,Fault}; position:{F1,F2,F3}; button_F1:boolean; …… door_F1:{Opening,Opened,Closing,Closed}; door_F2:{Opening,Opened,Closing,Closed}; door_F3:{Opening,Opened,Closing,Closed}; passenger:{None,In,Out}; weight:{None,Normal,Overload}; arrived:boolean; emergency:boolean; ASSIGN init(state) := Idle; init(passenger):=None; …… next(position):=case position=F1&state=Up:F2; position=F2&state=Up:F3; position=F2&state=Down:F1; position=F3&state=Down:F2; door_F1=Closed&(!button_F1)&position=F1 &state=Up:F2; door_F3=Closed&(!button_F3)&position=F3 &state=Down:F2; door_F2=Closed&(!button_F2)&position=F2 &state=Up:F3; door_F2=Closed&(!button_F2)&position=F2 &state=Down:F1; TRUE:position; esac; next(state):= case state=Idle&(door_F1=Opening&passenger=In &weight=Normal): Waiting; state=Idle&(passenger=In&weight=Overload): Warning; state=Waiting&(passenger=In&weight=Normal&(button_F2|button_F3)): Up; state=Waiting&(passenger=In&weight=Normal& button_F1|button_F2): Down; state=Waiting&emergency:Stop; …… esac; 上述代码是对电梯模型的一个描述，代码中有几处省略部分，其中第一处是button_F2,button_F3, request_F1,request_F2,request_F3的数据类型，为boolean型，第二处是weight,button_F1,button_F2, button_F3,door_F1,door_F2,door_F3,arrived的初始化描述。第三处省略的部分是对电梯状态state和按钮状态door_F1,door_F2,door_F3的条件选择结构。

5.2 属性规约提取与验证 属性规约是系统运行过程中必须满足的规范，其保证了系统的一致性和安全性。针对于本文提到模型，主要从以下几个方面进行验证: (1)安全性。一个系统的运行首先要保证其安全性，对此要验证的是：在未来的任意一个时刻，电梯系统都不会把乘客困在电梯中。

(2)前向一致性。电梯系统的运行需要满足前向一致性。对此验证电梯初始状态为空闲状态时，当有乘客进入时，未来的某一状态会由于超重导致电梯报警。

(3)可达性。对此要验证电梯系统的自动机模型是否可以到达任何一个图中描述的状态。

(4)陷阱性质。根据自动机图中描述的状态变迁，人为增加一条和某一行为需求描述相似的变迁，对其进行取反操作，观察模型检验能否检测出相似且不一致的行为。对此要验证当有乘客在一楼且按下上行按钮后，电梯不会出现上行状态。检测结果如表5.2所示。

表5.2 性质验证结果 待验证性质 CTL性质描述 验证结果 安全性 SPEC AF (passenger=In->AG passenger=Out) true 前向一致性 SPEC AF(state=Idle&passenger=In->EF state = Warning) true 可达性 SPEC AF(state=Idle -> AG state=Warning) false 陷阱性质 SPEC AG (position = F1&state = Up ->AX position != F2) false 上表是对以上几个属性规约性的表述。图5.3, 5.4是NuSMV的验证结果。下面对NuSMV的验证结果进行分析。

(1)安全性的CTL描述是在所有正常情况中，乘客不能被困在电梯中，结果显示是true，证明该电梯模型具有安全性质。

(2) 前向一致性。结果显示是true。表示在模型转换过程中状态前后的变迁关系是正确的，说明按照本文的转换规则从自然语言转换的自动机模型是可信的。

(3)可达性的表述为，按照需求定义的功能判断整个系统中的某个状态是否可达，结果显示false，反例的出现说明了与预期不一致的行为，帮助构建更为完善的需求模型。

(4)陷阱性质。结果显示是false。表示能够检测出需求描述不一致的行为。反例的出现首先说明了能够检测出与描述不一致的行为，其次，根据反例提供的路径信息可以进一步分析模型的内在联系，帮助构建更为全面的需求模型。

图 5.3验证结果1 图5.4验证结果2 事实上，当变换越所面临的状态越多时，则所需要遍历的路径也就越多，不仅工作量大，而且容易忽略一些状态变换；
而模型检验可以自动的遍历所有状态，遇到与预期性质不一致的情况时自动生成一条反例。通过分析反例得出通过自然语言建立的模型的不足之处，以供继续分析完善模型。另一方面，当模型的状态空间变得足够大时，人工的方法几乎已经无法解决状态的遍历问题，只能依靠自动或者半自动的方法，这也是模型检验的优势所在。

5.3 需求冲突消解 在5.1节中给出的电梯系统模型基础之上，假设电梯系统此时由于需求有所改变增加一条新的需求“全自动化”，即为了更加智能化增加“所有电梯操作均能通过智能声控设备完成”。

对原文中加入新需求增加SMV描述如下：
autostate:{up,Down,Hold,Stop} next(autostate):case autostate:up&(arrived&door_F1=Opening|door_F2=Opening|door_F3=Opening)&passenger=Out):Hold; autostate=Down&(arrived&(door_F1=Opening|door_F2=Opening|door_F3=Opening)&passenger=Out):Hold; autostate=Hold&emergency:Stop; TRUE: autostate; esac; 提出的属性规约是：
SPEC !AF(state =Stop & handle=FALSE&emergency=TRUE -> EG state = Idle ) 通过模型检验工具得出一条反例如图5.5所示。

图5.5模型检验结果 由反例可以得出一个条路径，分析路径可以看出最后得出的repair和handle状态均标记为false，与此关联的状态是stop和fault。

可以解释为自动化操作无法处理电梯的这些状态状态。根据 4.2.3节提出的需求关联度方法，autostate的状态关联有4个，原集有8个状态。根据本文公式4-(1)关联度为1/2。与stop和fault关联的状态有有6个，根据公式4-(1)其关联度为2/3。则根据需求关联度的方法，应该对autosate这个需求进行重新考虑，考虑将其删除或者精化。

5.4小结 本节在电梯系统实例基础上，对本文提出电梯系统的需求进行了一致性验证，验证了本文提到的方法的可行性。除此之外，对于需求冲突消解类问题，在电梯系统中使用本文提到需求冲突消解方法进行分类并使用相应的方法进行消解，达到了预期的目标。

第六章 总结与展望 6.1 总结 本文主要研究了一种基于模型检验的需求不一致及需求冲突消解的方法，通过分析目前现有的需求不一致的方法，提出了一个新的基于模型检验和自然语言相结合的需求不一致研究框架，并使用所提出的模型框架进行了一致性的验证。除此之外，对于需求冲突消解问题，提出使用需求关联度的方法解决功能性需求冲突，对于非功能性的需求，提出权衡策略解决冲突，对于不可度量的非功能需求，使用基于经验的方法解决冲突，对于可度量的方法，使用代价权衡策略的方法综合比较得出最优的代价策略。最后，本文通过一个电梯系统实例验证了可行性分析和有效验证。

通过本文的研究完成了一下目标和内容：
（1）
同过分析现有的需求不一致建模方法和应用，提出一个新的基于模型检验的需求不一致研究框架。

（2）
对自然语言进行分解提取，利用相似度算法计算出自然语言描述的相似性，解决模型检验不能定位的问题。

（3）
提出了一套完整的模型提取及转换的方法，从基于自然语言的描述进行分类提取，转换成自动机模型，然后由自动机模型转换成模型检验能够自动识别的语言，使用模型检验工具进行自动的识别。

（4）
对于冲突消解，本文给出了两种不同类别的冲突消解方法。对于功能性需求冲突的消解问题，使用需求关联度的思想，将关联度低进行舍弃或者精华，从而消解掉需求冲突。、 （5）
对于非功能需求冲突，提出使用代价权衡策略进行分析，综合考虑其策略代价和成本代价，从经济学的生产理论进行分析考虑，从而消解非功能需求冲突。

（6）
结合电梯模型的实际案例，证实了基于模型检验的需求不一致模型的有效意义。并在电梯模型的基础上实现了本文提及的一致性验证和需求冲突的处理问题，验证了本文研究的可行性和有效性。

6.2 展望 本文在基于模型检验的需求不一致问题的研究和需求冲突消解虽然取得了一定的成果，但是仍然存在一定的局限性，需要进一步的进行一下研究：
（1）
本文提出的基于模型检验的需求不一致问题研究，只在文中涉及的自然语言和相应的模型基础之上进行了分析，下一步应该继续完善和改进模型，使其具有更高的普遍性。

（2）
本文对于需求冲突消解给了比较合理的方法，对发生的需求冲突进行分类后采用不同的方法进行消解，但是考虑的方面还是不够。例如本文没有详细说明如何使用模型检验和自然语言对功能性需求和非功能性需求分类，下一步考虑在在自然语言处理中引入对属性的分解，在模型检验中引入时间自动机等概念来更好的表示非功能性需求，另外，对于某些可以度量的非功能需求的约束除了最低约束，还有最高约束，下一步工作是也要对这些约束进行更加深刻的研究。

（3）
本文电梯实例相对比较简单，并没有包含更加复杂的系统功能，下一步的工作将要研究更加复杂的系统，将本文的研究内容应用于复杂的实际项目中，以更好的验证方法的可行性。

参考文献 [1] Leffingwell D, Widrig D. Management Software Requirements：A Unified Approach[M]. New Jersey:Addison-Wesley, 2000. 65-72 [2] Pandey D, Suman U, Ramani A K. An effective requirement engineering process model for software development and requirements management[C]//2010 International Conference on Advances in Recent Technologies in Communication and Computing. IEEE, 2010:287-291. [3] 毋国庆等.软件需求工程[M].北京:机械工业出版社,2008,8. [4] urkiewica J, Nawrocki J, Ochodek M, et al.HAZOP-based identification of events in use cases[J]. Empirical Software Engineering, 2015,20(1):82-109 [5] Nuseibeh B, Easterbrook S, Russo A. Leveraging inconsistency in software development[J]. Computer, 2000, 33(4): 24-29. [6] Walter B , Hammes J , Piechotta M , et al. A Formalization Method to Process Structured Natural Language to Logic Expressions to Detect Redundant Specification and Test Statements[C]// Requirements Engineering Conference. IEEE, 2017(38): 263-272 [7] Heitmeyer C L , Jeffords R D , Labaw B G . Automated consistency checking of requirements specifications[J]. Acm Transactions on Software Engineering & Methodology, 1996, 5(3):231-261. [8] Van Lamsweerde A , Letier E . Handling obstacles in goal-oriented requirements engineering[J]. IEEE Transactions on Software Engineering, 2000, 26(10): 978-1005. [9] Glinz M . A lightweight approach to consistency of scenarios and class models[C]// Requirements Engineering, 2000. Proceedings. 4th International Conference on. 2000:49-58 [10] K. Lee and S. Lee. Applying Game Theoretic Approach to Goal-Driven Requirements Trade-Off Analysis for Self-Adaptation, 2015 IEEE 39th Annual Computer Software and Applications Conference, Taichung, 2015, pp. 330-335. [11] Applying fuzzy preference relation for requirements prioritization in goal oriented requirements elicitation process [J]. International Journal of System Assurance Engineering and Management, 2014, 5(4): 711-723. [12] Suhaib M, Ohnishi A. Potential Conflicts Identification among Sub Goals in Goal Oriented Requirement Analysis Using Matrix[J]. International Journal of Progressive Sciences and Technologies (IJPSAT), 2018, 10(2). [13] Gulzar K, Sang J, Ramzan M, et al. Fuzzy approach to prioritize usability requirements conflicts: An experimental evaluation[J]. IEEE Access, 2017, 5: 13570-13577. [14] Hassine J, Amyot D. An empirical approach toward the resolution of conflicts in goal-oriented models[J]. Software & Systems Modeling, 2017, 16(1): 279-306. [15] Zhang W, Deng Y. Combining conflicting evidence using the DEMATEL method[J]. Soft computing, 2019, 23(17): 8207-8216. [16] 朱雪峰, 金芝. 关于软件需求中的不一致性管理[J]. 软件学报, 2005(07):28-38. [17] 张建, 吴俊, 方景龙. 模型自动转换与一致性验证方法[J]. 计算机工程与设计, 2017(9). [18] 周宇, 黄延凯 et al. 一种开放环境下软件在线演化一致性验证方法[J]. 软件学报, 2015, 26(4):747-759. [19] 张璇, 王旭, 李彤, et al. 软件非功能需求权衡代价[J]. 软件学报, 2017(5). [20] 李瑞轩, 鲁剑锋, 李添翼, et al. 一种访问控制策略非一致性冲突消解方法[J]. 计算机学报, 2013(06):88-101. [21] 湛浩旻, 印桂生, 赵蕴龙. 基于ISM与AHP组合的需求优先级排序方法%Method of Prioritizing Requirements Based on the Combination of ISM and AHP[J]. 计算机科学, 040(3):225-227,243. [22] 王守堰, 金英, 张晶. Nash equilibrium strategy choosing method for resolving inconsistencies of requirements%一个用于解决需求不一致的纳什均衡策略选取方法[J]. 计算机应用研究, 2015, 000(002):466-469,474. [23] Spanoudakis G , Finkelstein A , Till D . Overlaps in Requirements Engineering[J]. Automated Software Engineering, 1999, 6(2):171-198 [24] Xu Haoguang, Wang Ning, Liu Jiaming, et al. C-omprehensive Computation Algorithm of Similarity f-or Natural Language Retrieval [J]. Computer system application, 2017, 26(6):170-175. [25] Cong Y , Chan Y B , Ragan M A . A novel align-mentfree method for detection of lateral genetic t-ransfer based on TF-IDF[J].Scientific Reports, 2016, 6(30308):1-13. [26] Rui S , Deming Z . Translating software requi-rement from natural language to automaton[C] // Int-ernational Conference on Mechatronic Sciences. IEEE, 2014:2456-2459. [27] Jin Huan, Huang Qing. Requirement formal modeling and quality characteristics verification based on scene behavior [J]. Computer Applied Research, 2016, 33(5):1384-1398. [28] Huang Wudan, Chen Zhe. Model Checking of Secu-rity Issuses in Border Gateway Protocol [J]. Journ-al of Chinese Computer Systems ,2017,38(6):1188-1191. [29] Li Jiali, Chen Yongle, Li Zhi, et al. RTSP protocol vulnerability mining based on protocol state grap-h traversal [J]. Computer Science, 2018, 45 (9): 171-176. [30] He Yang, Hong Mei, Qi Linying, et al. Functional test case generation method based on model checking tool NuSMV [J]. Computer application, 2015 (A02): 155-159. [31] Li Xin. ASchedulingStrategy of TargetLayerReservationElevatorGroupBasedonModelCheckingMethod [D].Nanchang:Jiangxi University of Finance and Economics: 2018:11-54. 致 谢 研究生的生活接近尾声，在这三年的时间里，我的导师xxx教授无论在学习上还是生活上中都给与了我各种指导和帮助。xxx老师一步一步的引导我做研究，如何选择文献，怎样精读文献，怎样泛读文献，引导我自己从中发现问题，再进一步指引我提出解决办法，并在魏老师的悉心指导下完成了本篇论文。

除了做研究外，我的导师还教会了我如何做一名研究生，怎样更好的杜工研究生时代，合理安排时间，在学习之余让自己的研究生生活证据丰富多彩，并教会了我为人处事的道理，这将让我在以后的工作和学子中收益终身。在此由衷的对魏老师说一声谢谢！ 在完成该论文的过程中，师哥师姐都给了我很多的帮助。师哥师姐帮助我查文献，提供参考书籍，分享他们的经验教训，让我在论文撰写中少走了很多弯路；
在此感谢他们的帮助。另外，我的研究生生活还有必不可少的还有同班同学，是他们让我研究生的生活变得更有意义。

还要感谢一直都在支持我鼓励我的父母和家人们，为了培养我，我的父母付出了很多，无论遇到什么困难他们都是我坚强的后盾，希望他们能身体健康。

最后，感谢评阅论的每一位老师，感谢各位老师对我的论文提出的宝贵的意见和指导，谢谢！