An Approach to UML Consistency Checking Based on Compositional Semantics

One of the ways to specify dynamic behavior in UML is to model interactions between objects with sequence diagrams, and model the behavior of each object with state machines. In this context, the problem of ensuring consistency between the sequence diagrams and state machines may arise. To verify consistency, the authors propose an approach based on compositions of Büchi automata which allow us to capture the evolution of each object among the lifeline. This paper focuses on UML modeling and verification methods and bridges the gap between theoretical studies on formal semantics and practical studies to implement languages through model transformations. The transformations include basic interactions, state invariants, strict and weak sequencing, and alternative interaction fragments. Ultimately, the results of the transformations are integrated into the Spin model checker as a never claim property. The authors use the Automatic Gate Controller Railway (AGCR) as an example to illustrate their approach.