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

作     者：Besnard, Valentin Teodorov, Ciprian Jouault, Frederic Brun, Matthias Dhaussy, Philippe 

作者机构：ESEO TECH ERIS Angers France Lab STICC UMR CNRS 6285 ENSTA Bretagne Brest France 

出 版 物：《SOFTWARE AND SYSTEMS MODELING》 (软件与系统模块)

年 卷 期：2021年第20卷第6期

页      面：1825-1855页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Davidson Consulting French Directorate General of Armaments (DGA) European Regional Development Fund (ERDF) of the EU Brittany Region Departmental Council of Finistere and Brest Metropole, Cyber-SSI project 

主　　题：Model-checking Monitoring Model interpretation Embedded systems Observation Language Synchronous Composition Model-driven software engineering Software verification Model checking Interpreters Embedded software 

摘      要：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 Buchi 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.