Distributed Runtime Verification for EMF Models and Model Transformations

for Degree: 
Contact Person: 
Status: 
Available

The implementation of distributed systems with general-purpose programming languages is a complex and error-prone task. Modelling frameworks like EMF [1] can be used to create Domain-Specific Languages (DSL) tailored to these scenarios, reducing both the effort and the possibility of introducing bugs. However, this technique does not shield from specification mistakes. Integrating Runtime Verification (RV) into the process allows to monitor the distributed system during its execution and react to failures [2].

Problem Statement
We developed a DSL for the specification of distributed collaborative scenarios for autonomous agents. This specification, in the shape of EMF model, can be automatically deployed, as well as simulated through model transformations that manipulate the agents. (See the project's website for a video and more information.) Using our adaption of Linear Temporal Logic [3] for real-time properties and distributed scenarios, we can define temporal properties to check the correctness of the distributed system. These properties can also be evaluated by representing them as models and using model transformations, which allows to evaluate the properties along the simulation of the system. The goal of this thesis is to implement this evaluation of such properties as model transformations in EMF.

Goals

  • Work your way into EMF, our DSL editor and model transformation languages.
  • Implement our LTL semantics as model transformations.
  • Run tests with different distributed scenarios and correctness properties.

Requirements

  • You have some knowledge in declarative programming and formal languages and you either already know about runtime verification (e.g. CS4139) or you are at least interested in formal methods.
  • You are not afraid of working between two different areas of research.

Høgskulen på Vestlandet (HVL)
This thesis will be done in close collaboration with the ICT Engineering Department at the HVL in Bergen. The communication with your co-workers and your thesis will be in English. The thesis can be combined with an ERASMUS stay in Norway.

Literature
[1] Eclipse Modeling Framework, http://www.eclipse.org/modeling/emf
[2] F. Macías, T. Scheffel, M. Schmitz, R. Wang: Integration of Runtime Verification into Metamodeling for Simulation and Code Generation (Position Paper). RV 2016: 454–461
[3] Martin Leucker: Teaching Runtime Verification. RV 2011: 34–48