%0 Conference Proceedings
%T Verifying and Monitoring UML Models with Observer Automata: A Transformation-Free Approach
%+ ESEO-ÉRIS (ÉRIS)
%+ Lab-STICC_ENSTAB_ CACS_MOCS
%A Besnard, Valentin
%A Teodorov, Ciprian
%A Jouault, Frédéric
%A Brun, Matthias
%A Dhaussy, Philippe
%< avec comité de lecture
%( 2019 ACM/IEEE 22nd International Conference on Model Driven Engineering Languages and Systems (MODELS)
%B 22nd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2019
%C Munich, Germany
%P 161-171
%8 2019
%D 2019
%R 10.1109/MODELS.2019.000-5
%K Embedded Systems
%K Model Interpretation
%K Monitoring
%K Observer Automata
%Z Engineering Sciences [physics]
%Z Computer Science [cs]/Software Engineering [cs.SE]Conference papers
%X 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.
%G English
%2 https://hal.science/hal-02433749/document
%2 https://hal.science/hal-02433749/file/besnard2019.pdf
%L hal-02433749
%U https://hal.science/hal-02433749
%~ UNIV-BREST
%~ INSTITUT-TELECOM
%~ ENSTA-BRETAGNE
%~ CNRS
%~ UNIV-UBS
%~ ENSTA-BRETAGNE-STIC
%~ ENIB
%~ LAB-STICC
%~ ESEO-TECH
%~ INSTITUTS-TELECOM
%~ ESEO-ERIS