Unified verification and monitoring of executable UML specifications: A transformation-free approach.

The increasing complexity of embedded systems renders software verification more complex, requiring monitoring and formal techniques, like model-checking. However, to use such techniques, system engineers usually need formal expertise to express the software requirements in a formal language. To facilitate the use of model-checking tools by system engineers, our approach uses a UML model interpreter through which the software requirements can directly be expressed in UML as well. Formal requirements are encoded as UML state machines with the transition guards written in a specific observation language, which expresses predicates on the execution of the system model. Each such executable UML specification can model either a Büchi automaton or an observer automaton, and is synchronously composed with the system, to follow its execution during model-checking. Formal verification can continue at runtime for all deterministic observer automata used during offline verification by deploying them on real embedded systems. Our approach has been evaluated on multiple case studies and is illustrated, in this paper, through the user interface model of a cruise-control system. The automata-based verification results are in line with the verification of the equivalent LTL properties. The runtime overhead during monitoring is proportional to the number of monitors. [ABSTRACT FROM AUTHOR]