Formal specification of the UML sequence diagram using Z notation
Jing Li · Jounal of Xidian University · 2002
The lack of precise semantics of UML makes it difficult to support consistency check and accuracy analysis of the models of large, complex systems. It is an effective way to resolve this problem to apply existing formal techniques to UML. In this paper, using a formal specification language Z, the authors present a rigorous semantics of the UML sequence diagram, define its abstract syntax, wellformed rules and consistent constraints that it must satisfy, and demonstrate with a practical example that this work lays a foundation for the rigorous semantic analysis and validation of the UML sequence diagram.