【作者】 刘洋；

【导师】 吴尽昭；

【作者基本信息】 电子科技大学 ， 计算机软件与理论， 2013， 博士

【摘要】 需求验证一直以来都是软件开发过程中非常重要的一个环节，软件需求的正确性直接影响着后期开发工作中人力、物力和资源的消耗。随着网络技术的发展，一种部署在网络环境中的复杂软件系统—网络式软件产生了，其拓扑结构和软件行为可以动态演化，因此，对传统的需求验证方法提出了新的要求。形式化方法通过对系统进行严格的语法和语义定义，使得分析和推理能够精确化、数学化，从而能够完备的证明系统是否正确实现了设计者的意图。网络式软件需求模型的验证主要针对目标模型和过程模型，在973项目“需求模型验证与管理”（2007CB310803）的支持下，本文针对网络式软件需求模型目标层和过程层的特点，充分利用已有的形式化规约语言和分析方法对其进行形式化方法的研究。主要工作包括以下几个方面：1.针对因网络式软件复杂性而带来的需求获取信息不协调性难以避免的特点，提出应用极大协调子集的思想进行不一致信息的处理；针对处理后的信息，在目标层模型思想的指导下，建立了一种新的描述需求目标性质和目标之间关系的GM模型，给出了GM模型正确性和完整性分析方法，以及相关验证算法，并设计了动态环境下目标模型演化的相关规则。该方法可以刻画目标层中所有目标之间的关系，包括低层目标之间的关系和高层目标之间的关系，并能融合用户需求之间的不一致信息，保留需求初期还未能确定的系统目标。2.在深入研究Z语言和Petri网特点的基础上，扩展了集成Petri网和Z语言的PZN模型，并将它应用于网络式软件需求过程模型的建模分析，给出了PZN模型的活性、可达性和完整性具体分析方法，基于PZN模型对过程模型进行形式化建模和分析，利用PZN中所含的Petri网性质分析过程模型的活性和可达性，通过PZN中的Z框架描述分析过程模型的完整性，同时，给出了动态环境下，过程模型的增加、减少、模块划分等变化规则。3.为了保证过程模型同已确认的需求目标及业务规则的一致性，在分析原子目标和原子过程的映射关系的基础上，分析了整个目标模型与过程模型间的相互关系，提出了目标层与过程层的一致性定义及其分析方法，以保证过程模型能够正确的实现用户需求目标，以及需求分析过程中目标与过程的统一。本文在网络式软件需求验证的形式化方法上的研究成果，能有效的刻画用户需求的功能属性和非功能属性，有利于提高需求分析阶段的正确性和完整性，降低软件中因为用户需求的不正确而带来的错误以及资源的损失，提高软件开发的效率。同时，本文作者参与了所在团队网络式软件需求模型验证器的开发，实现了本文中的需求验证方法，并对项目实例进行验证，实例显示本文的方法具有很好的效果。更多还原

【Abstract】 Requirements verification has been a significant phase during the softwaredevelopment, and the correctness of the software requirements directly affects theconsumption of human and material resource during the later stage of softwaredevelopment. With the rapid development of networked technology, a complexsoftware system, named networked software, which is deployed on networkenvironment, appears. Its topology structure and behavior can evolve dynamically. So,the new demand on requirements verification method has been put forward. The mostnotable feature of formal methods is that they are mathematically based on syntax andsemantic. And it also can be used to exactly analyze, reason and completely provewhether the system realizes the intention of the designer or not.Requirements verification of Requirements Meta-Modeling Frame for NetworkedSoftware(RGPS) mainly aims at the goal layer and the process layer. Under the supportof973project “Requirements Models Verification and Management”(2007CB310803),according to the characteristics of the goal layer and the process layer, we study on theformal verification methods by making full use of existing formal specificationlanguages and analysis methods. The main contributions include the following aspects:1. It is very difficult to avoid the inconsistency of requirements informationsbecause of the complexity of networked software, however, we propose a method thatuses maximally consistent subset to handle those inconsistent informations; under theguidance of the goal layer, we present a new model, named GM model, to describe theproperties and the relations of the requirement goals; we give the analysis methods forvalidity, integrity, and algorithms for verifying completeness and correctness; we alsoprovide corresponding rules of model evolution under dynamic environment. Thismethod can be used to effectively depict the relationships between goals of the wholemodel, including the lower goals and the top goals. It also can be used to fuse thedifferences among users’ requirements, and moreover, keep the indeterminacy in theearly stage.2. Base on Z language and Petri nets, we expand the integrated specification named PZN model, use it to model the process layer of the networkded software, andgive the analysis methods of its activity, accessibility and integrity; we construct theformal modeling of process model based on PZN model, and give the formal analysisof the process model; we analyze the activity and accessibility of the process model bythe Petri nets properties, and analyze the integrity of the process model by Zframework; we also give the corresponding rules under dynamic environment, such asmodel increasing, decreasing, and division.3. In order to ensure the consistency between the confirmed requirements andbusiness rules in the process model, based on analyzing the mapping relationshipsbetween atomic goals and atomic processes, we analyze the relationships between thewhole goal model and the process model, and propose the definition of consistency andanalysis method, to ensure that the process model can realize the users’ demandscorrectly and unify the goal and the process during the requirements analysis.The study on formal methods of networked software requirement verification,effectively depict the functional and nonfunctional requirements from users,comprehensively guarantee the correctness and completeness, reduce the errors andresources loss caused by the incorrect requirements, and improve the efficiency ofsoftware development. At the same time, the author of this dissertation participates indeveloping the Networked Software Requirements Model Verifier1.0to implement therequirements verification methods proposed in this sissertation. The project instancesshow that the methods presented in this dissertation have a good effect on requirementsverification.更多还原