Research And Application Of Model Consistency Verification Based On State Reduction

With computer hardware and software system increasingly complex and the application ofconcurrent system, how to assure the correctness and consistency become significant. Thetask-oriented integrated design approach was taken as the research background. The approach has themodeling characteristics of large scale, complex structure, and allowing multiple designers to designcollaboratively which may lead to model inconsistentency. In recent years, the approaches by usingformal methods to describe system models and model checking techniques to verify modelconsistency were studied by many scholars. However, the existing methods may have someinadequateness. An appropriate definition of the consistency lacks between class diagrams, sequencediagrams and state machine diagrams. The redundancy elements in the state machine diagram thatindependent of consistency can significantly affect the efficiency of the consistency verification ofcomplex model. The current methods that transform system models to the modeling languagePROMELA are lack of supporting some diagrams, model structures and consistencies. In order toimprove these deficiencies, the main work is as follows.First, considering the elements of UML class diagram, sequence diagram, state diagram and withthe analysis of the model’s behavioral characteristics, the new definition of behavioral consistencywas proposed. For there are a large number of redundant states and transitions in the state machinediagram, the reduction rules and algorithms were discussed in detail for null transitions, unreachablestates, pseudo states and composite states. Experiment showed that the algorithm reduces thecomplexity of the model to verify, cuts down the states and transitions’ quantity effectively in theprocess of verification and improves the efficiency of verification.Then, for lack of supporting in class diagram, multiple interactions of sequence diagram, complexstructure of UML sequence diagram and state diagram and the behavioral consistency in the currentmodel transformation methods, the transform method of UML model into PROMELA based onprocess synchronization was present and the transformation algorithm was designed with the analysisof PROMELA modeling features. Experiments showed that the behavior consistency of UML modelswas verified effectively by this method. Moreover, the method supports class diagram, multipleinteractions and combined fragments of sequence diagram, state diagram with complex structure. Bycomparing with six methods of recent literature, it showed that the method has good advantage insupporting complex model structure and consistency compared with the current ones.Finally, according to the reduction algorithm of state machine diagram and the transformationalgorithms based on process synchronization, the system design tool based on the integrated designplatform was designed. The tool implemented the UML modeling and the model verification modules.Through the "Offensive System" experiments, the results showed that the system design tool detectedthe inconsistency of models. In addition, according to the counterexamples, the inconsistency waseliminated.