Research On Formal Verification Methods Of Model Of Complicated Information System

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...