Dissertation > Excellent graduate degree dissertation topics show

Research on Formal Verification Methods of Model of Complicated Information System

Author: ZhangTao
Tutor: HuangShaoBin
School: Harbin Engineering University
Course: Applied Computer Technology
Keywords: Formal Method Model Checking Complicated Information System RAISESpecification Language Unified Modeling Language Timed Automata
CLC: TP311.52
Type: PhD thesis
Year: 2012
Downloads: 284
Quote: 1
Read: Download Dissertation

Abstract


Some problems on software quality and reliability have been existing for a long time.Although requirement analysis, design and test techniques are still the major means whichguarantee high reliability of software engineering, they can’t fully meet the requirement of thedevelopment of highly reliable software systems. Because people’s requirements for theability such as distributed processing, parallel processing, real-time processing of softwaresystem is increasingly improving, which makes software systems growing more and morecomplex. Model checking as a formal verification technique gets much attention fromacademia and industry, because of its strict mathematical basis, fully automated validationprocess and early successful application in the hardware system and protocol verification.However, applying model checking in various stages of software engineering is still in theexploratory stage, which can make a comprehensive and automated analysis and verify thecomplicated information system’s requirements, design and performance to improve softwaresecurity and reliability. According to the above problems, this dissertation combines formalmethods and model checking technique to make a research on modeling and formalverification technique of complicated information system whose behavior has distributed,concurrent and real-time characteristics from the perspective of requirement analysis level,model design level and performance design level.First, formal methods and model checking techniques have been reviewed in thisresearch. The behavior characteristics of complicated information system are illustrated andthe emphasis and difficulty of formal model and verification is analyzied. Then someproblems in this field and the future research are concluded.Second, to validate the correctness of the requirements design of complicatedinformation system, this research divides the software requirements into top-level andtechnical-level requirements, and uses behavior-oriented abstract modeling approach to modeldomain policies as top-level requirements of system, and specifies the requirement modelwith RSL. To validate and refine the top-level requirements model, this dissertation translatesthe RSL specification of the top-level requirements model into a Promela model by definingthe transformation rules of syntax and semantics of RSL. The property specification oftop-level requirements model is encoded to temporal logic formula. Finally, using the modelchecker SPIN automatically verifies whether the top-level requirements model can satisfy thetemporal logic formula. Third, to validate the correctness of technical-level requirements design, UML sequencediagrams are used to model the interactive scenes of complicated information system.Because UML sequence diagrams model lacks of accurate dynamic semantics, and can notautomatically validate the dynamic nature of the model, this dissertation defines operationalsemantics of transition system for UML sequence diagram and defines its transformation rulesfrom UML sequence diagram to promela model. The parse result of XML file of sequencediagrams is converted to promela program. At last, the promela program which describes thesystem requirements and linear temporal logic which describes the specification of system areused to be the input of model checker SPIN automatically validating the correctness oftechnical-level requirements design of systems.Forth, to validate the correctness of design model of complicated information system,UML statecharts are used to be the major modeling tool. The middle representation of theUML statecharts which transform hierarchical statecharts to flat statecharts is given bydefining the major elements of UML statecharts with tuple. On the basis of middlerepresentation, the operational semantics of UML statecharts is defined, the transformationrules from complicated information system’s design model to NuSMV input model aredesigned. Based on this transformation rules and the parse result of XML file of UMLstatecharts, the automatic transformation process from design model to NuSMV input modelis realized. The correctness of the transformation process is illustrated by proving thebisimulation equivalence relation between the operational semantics of UML statecharts andNuSMV input model which is generated by transformation rules. Finally, the model checkerNuSMV is used to verify whether the design model of complicated information system cansatisfy the property specification.Furthermore, this dissertation makes a research on fomal verification technique ofreal-time performance design of complicated information system. The task architecture whichdescribes the activating order of internal event and task when external event arrives is createdby UML collaboration diagram in the requirement process. Then the execution time budget ofconcurrent task is allocated by events order analysis method and the UML collaborationdiagram is extend to real-time collaboration diagram. Ultimately, the timed automata networkis established on the basis of real-time collaboration diagram, and is input into the modelchecker UPPAAL for automated verification.In the end, the work of the dissertation is concluded and the further research direction isput forward

Related Dissertations

  1. Software Testing and Reliability Computing Based on Model Rebuilding,TP311.53
  2. Design and Implementation of Educational Management Information System for WeiFang Professional College,TP311.52
  3. Design and Implementation of Mobile Newspaper System,TP311.52
  4. Design and Implementation of Online Social Insurance Declaration System,TP311.52
  5. Analysis and Design of Comprehensive Taxation Management Information System,TP311.52
  6. Enterprise Remote Monitoring Management System Design and Implementation,TP311.52
  7. Compositional Verification Through Learning and Assume-Guarantee Rules,TP311.52
  8. University Examination Management Information System Design and Implementation,TP311.52
  9. Qu Plastics Group Human Resource Management Information System Analysis and Design,TP311.52
  10. The Analysis and Design of Management System for Pattern Approvla of Measuring Instruments,TB9
  11. GIS data model based on digital terrestrial systems and implementation of applied research,P208
  12. Simulation and Analysis of Schedule Strategy of Reconfigrable HW System,TN791
  13. Research and Implementation of Armory Management Information System,TP311.52
  14. Disc Chain System Design and Implementation of the lease,TP311.52
  15. Component-based Formal Development for Reuse,TP311.52
  16. Design and Implementation of the integrated management system of the engine room of UML - based,TP311.52
  17. The Design and Practice of Ningxia Telecom Business Navigator System,TP311.52
  18. Analysis and Design on Standard of Education Resource management Systems Based on the SCORM Standard,TP311.52
  19. The Application and Implemenation of PPTL Model Checking Tool,TP311.52
  20. Family planning propaganda analysis and design of interactive games,TP311.52
  21. Law Risk Management Information System’s Design and Implement,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