Verifying and Monitoring UML Models with Observer Automata: A Transformation-Free Approach

Valentin Besnard (1) , Ciprian Teodorov (2) , Frédéric Jouault (1) , Matthias Brun (1) , Philippe Dhaussy (2)

1 ÉRIS - ESEO-ÉRIS
2 Lab-STICC_ENSTAB_ CACS_MOCS

The increasing complexity of embedded systems renders verification of software programs more complex and may require applying monitoring and formal techniques, like model-checking. However, to use such techniques, system engineers usually need formal experts to express software requirements in a formal language. To facilitate the use of model-checking tools by system engineers, our approach consists of using a UML model interpreter with which the software requirements can directly be expressed as observer automata in UML as well. These observer automata are synchronously composed with the system, and can be used unchanged both for model verification and runtime monitoring. Our approach has been evaluated on the user interface model of a cruise control system. The observer verification results are in line with the verification of equivalent LTL properties. The runtime overhead of the monitoring infrastructure is 6.5%, with only 1.2% memory overhead. © 2019 IEEE.

Mots clés: Embedded Systems; Model Interpretation; Monitoring; Observer Automata

Domaines: Sciences de l'ingénieur [physics]; Génie logiciel [cs.SE]

Valentin Besnard, Ciprian Teodorov, Frédéric Jouault, Matthias Brun, Philippe Dhaussy. Verifying and Monitoring UML Models with Observer Automata: A Transformation-Free Approach. 22nd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2019, 2019, Munich, Germany. pp.161-171, ⟨10.1109/MODELS.2019.000-5⟩. ⟨hal-02433749⟩