Study On Formal Methods Of Networked Software Requirements Verification

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.