Based On Model Checking The Model-driven System For The Design And Realization

AutoPG is a set of model-based analysis tools for detecting UML,and it is used to analyse Sequence Diagram in UML,has a solid, reliable foundation of the theory.This paper presents the design and development of autoPG version 1.0,which implements the conversion from the UML Sequence Diagram model to the model checking language called Promela program and implements the model verification.UML sequence Diagram consisits of messages from objects,can be exported to xml format files through MagicDraw.AutoPG will analyse this xml file,including accesssing concrete information in the diagram and convert it to the model checking language called Promela, and eventually call SPIN,a model checking tool,to verify and validate the correctness of the model.Once the model is checked to be correct,it will contribute to the follow-up development of software systems to improve the accuracy of the software system. The final article will be the actual case on how to use autoPG to generate Promela program and check the model.