Empowering Multilevel DSMLs with Integrated Runtime Verification

TL;DR

This paper presents a novel approach combining multilevel modeling and runtime verification in Model-Driven Software Engineering, enabling formal specification and correctness checking of complex distributed real-time systems.

Contribution

It introduces an integrated framework that merges MLM and RV using model transformation rules, enhancing system simulation and correctness verification.

Findings

Effective combination of MLM and RV for distributed systems

Model transformation rules facilitate semantics and correctness evaluation

Supports simulation and real-time property checking

Abstract

Within Model-Driven Software Engineering, Domain-Specific Modelling has proven to be a powerful technique to specify systems and systems' behaviour in a formal, yet understandable way. Runtime verification (RV) has been successfully used to verify the correctness of such behaviour. Specifying behaviour requires managing various levels of abstractions, making multilevel modelling (MLM) a suitable approach for this task. In this paper, we present an approach to combine MLM and RV with an example from the domain of distributed real-time systems. The semantics of the specified behaviour as well as the evaluation of correctness properties are given by model transformation rules. This facilitates simulation of the system and checking against real-time temporal logic correctness properties.