Empowering Multilevel DSMLs with Integrated Runtime Verification

TitleEmpowering Multilevel DSMLs with Integrated Runtime Verification
Publication TypeConference Paper
Year of Publication2019
AuthorsMacias, F, Rutle, A, Stolz, V, Scheffel, T, Schmitz, M
Conference NameVORTEX
PublisherSpringer
Conference LocationEngland
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.

Bibtex: 
@inproceedings {1318,
	title = {Empowering Multilevel DSMLs with Integrated Runtime Verification},
	booktitle = {VORTEX},
	year = {2019},
	publisher = {Springer},
	organization = {Springer},
	address = {England},
	abstract = {<p>Within Model-Driven Software Engineering, Domain-Specific Modelling has proven to be a<br>
	powerful technique to specify systems and systems{\textquoteright} behaviour in a formal, yet understandable<br>
	way. Runtime verification (RV) has been successfully used to verify the correctness of such<br>
	behaviour. Specifying behaviour requires managing various levels of abstractions, making<br>
	multilevel modelling (MLM) a suitable approach for this task. In this paper, we present an<br>
	approach to combine MLM and RV with an example from the domain of distributed real-time<br>
	systems. The semantics of the specified behaviour as well as the evaluation of correctness<br>
	properties are given by model transformation rules. This facilitates simulation of the system<br>
	and checking against real-time temporal logic correctness properties.</p>
},
	author = {Fernando Macias and Adrian Rutle and Volker Stolz and Torben Scheffel and Malte Schmitz}
}