Dissertation > Excellent graduate degree dissertation topics show

Study on Formal Methods of Networked Software Requirements Verification

Author: LiuYang
Tutor: WuJinZhao
School: University of Electronic Science and Technology
Course: Computer Software and Theory
Keywords: networked software requirements verification formal methods RGPS
CLC: TP311.52
Type: PhD thesis
Year: 2013
Downloads: 70
Quote: 0
Read: Download Dissertation

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.

Related Dissertations

  1. E-commerce Protocol Analysis and Verification Based on SPIN Model Checking,TP311.52
  2. Simulation and Analysis of Schedule Strategy of Reconfigrable HW System,TN791
  3. A Method for Formal Analysis of E-commerce Security Protocol,TP393.08
  4. Research on Software Requirement Specification Quality Model Based on Chinese Understanding,TP311.52
  5. Research and Application on Networking Software Development Method in the Field of Urban Traffic,TP311.52
  6. Formal Specification and Verification of Automatic DMARF System,TN912.34
  7. UPPAAL approach based interlocking control flow modeling and verification,U284.37
  8. A Study on Application of Value Engineering in Requirements Engineering of Software Project,TP31
  9. The Applied Research of PAR Method in Numerical Methods,TP311.52
  10. Security protocols based on strand space model analysis and validation password,O157.4
  11. A Heuristic Algorithm for Model-Checking Based on Counter Example Finding,TP311.52
  12. The Verification of Security Protocol Based on GSPM and the Inplementation of the Tool,TP393.08
  13. Formal Analysis of Security Protocols Based on Universally Composable Framework,TP393.04
  14. Towards Non-functional Requirements Analysis for Networked Software,TP311.52
  15. Formal Modeling and Verification for Component-Based Model Integrated CNC Systems with IEC 61499 Standard,TP311.52
  16. Key Techniques of Trustworthiness Improvement on Hybird Arithmetic Addition of Floating-point Fused Multiply-add Unit,TP302.1
  17. A Study on Formally Modeling and Verifying the Composition of Web Services,TP393.09
  18. Research on Formal Methods of Web Service Data and Service Composition Based on Process Algebra,TP393.09
  19. Research on Formal Design and Analysis for Security System,TP309
  20. Multi-Granularity Dynamic Characteristic Analysis of Networked Software,TP311.52
  21. The Research on Service Oriented Web Software Development Technology Based on Formal Method,TP311.52

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Software Engineering > Software Development
© 2012 www.DissertationTopic.Net  Mobile