Ying Zuo, Liang Dou, Lihua Xu, and Zongyuan Yang
Sequence diagram, Formalization, Mechanized semantics
UML Sequence Diagrams are widely used in software development. When putting to applications such as code generation, model simulation and other automated analysis, the formalization of UML Sequence Diagrams, especially correctness of it becomes increasingly important. This article presents the formal specification including denotational semantics and operational semantics of UML Sequence Diagrams. The Coq proof assistant is used to mechanize the semantics and prove the correctness of operational semantics compared to denoational semantics.
Important Links:
Go Back
