Liang Dou, Lunjin Lu, Zongyuan Yang, and Jinkui Xie
UML sequence diagrams, mechanized semantics, refinement, model development, Coq
Sequence diagrams are widely used to describe the behavior of software during the design phase. Sequence diagrams have significant practical value. However, a systematic way of understanding and specifying the formal semantics of sequence diagrams does not exist. Analyzing the design properties may reveal software faults before software implementation, thereby improving the software quality and reducing development costs. We propose to use the theorem proof assistant Coq to mechanize the semantics of sequence diagrams and the refinement relations on models. In this framework, the syntax of a sequence diagram is represented as inductive types, and the semantic function is represented as inductive predicates. Based on mechanized trace semantics, the desired properties of both semantics and the refinement relation can be stated as lemmas. The proof of each lemma ensures that the semantics and the refinement relation satisfy the specified properties. Our work demonstrates the viability of using Coq to mechanize the semantics of software design models and provide increased reliability guarantee in model-based development.
Important Links:
Go Back
