Formal Verification of Sequence Diagram with State Invariants Using Timed Automata

In a design model, the UML sequence diagrams typically play a crucial role in explaining the behaviors of the software system by showing the interactions between their objects. Especially, a sequence diagram with state invariants intentionally shows the appropriate runtime states of the objects at the particular points of time in their timelines. In practice, state-dependent behavior for an object is provided. An object responds differently to the same event depending on what state it is in. Moreover, due to the possibility of the hybrid uses of the synchronous and asynchronous interactions in this diagram, the nondeterministic situation may be unfortunately introduced, causing more complex and difficult to verify the final design. In this paper, we propose a formal verification method to ensure the basic properties of the design model drawn in these sequence diagrams with state invariants. A set of transformation rules are proposed to convert the original sequence diagram into its corresponding timed automata. The behaviors of the resulting timed automata would be simulated and verified using UPPAAL tool. Moreover, the behavioral properties, including deadlock, liveness, and safeness, of the design model are also formally verified using timed computation tree logic.