Formal specification and automated verification of UML2.0 sequence diagrams

Software reliability is with critical importance in security demanding areas, including space exploration, e-business and military defense. UML sequence diagrams capture the collaborations of objects, and bridge the gap between abstract design and coding. Hence studying formal methods and automated verification of sequence diagram is indispensible to assure software reliability. In this paper, we establish formal specification rules for UML2.0 diagrams based on CCS, calculus of communicating system. Based on those rules, we propose specification algorithm and prove its linear complexity. Hence formal specifications of sequence diagrams can be obtained with programmed algorithm. In the end, we use a case study to illustrate our approach and show how automated verification can help designer discover design mistakes in UML2.0 sequence diagrams.