Uml Sequence Diagram Of The Automatic Analysis Techniques

Nowadays, computers are used in all kinds of fields. In some important applications, the quality of the system is attached very high importance. Even a little error may cause great loss. After many years of engineering practice, it is realized that formal method is important for high confidence concurrent systems. Unified Modeling Language (UML) is a hotspot of researches in software engineering. UML sequence diagrams reflect the interaction and sequence of messages among the concurrent objects in the system, and hold the important position in software modeling.The main task of the thesis is to investigate the ways of automatically verifying concurrent systems. Firstly, the paper mainly introduces the principles, characteristics of model checking, and the ways to improve it. It also introduces the model checking tool SPIN, including its principles, syntax and techniques for optimizing. Then, the rules and methods of transforming UML sequence diagrams to PROMELA programs are presented. The method is used to verify the properties of UML sequence diagrams with SPIN to judge if designed models satisfy the key requirements of system. To improve the applicability of the method, extensible Markup Language (XML) format is used to define the external expression of sequence diagrams. To combine the verification with system design, a prototype of automatic verification tool for UML sequence diagrams has been designed and developed.