Formal Verification of UML Sequence Diagrams in the Embedded Systems Context

This paper shows a method for translating UML sequence diagrams to Petri nets and verifying deadlockfreeness, reachability, safety and liveness properties by using a model checker. In this proposed method, the user has not to know about temporal logics to describe the property to be verified. Instead, the user may adopt a high-level properties specification interface, which is automatically translated to a suitable temporal logic. We show the application of the proposed method in an embedded control application that consists of a sensory device mounted on a motorized platform that must detect and track specific objects in the environment.