You are here

Home › Research › Projects ›

Integration of Runtime Verification into Metamodeling

Runtime verification is an approach growing in popularity to verify the correctness of complex and distributed systems by monitoring their executions. Domain Specific Modeling Languages are a technique used for specifying such systems in an abstract way, but still close to the solution domain. We aim at integrating runtime verification and domain specific modeling into the development process of complex systems. Such integration is achieved by linking the elements of the system model with the atomic propositions of the temporal correctness properties used to specify monitors.

As an example of our approach consider a moving robot which can detect

  • obstacles with a distance sensor and
  • the border of the table with a color sensor.

In order to demonstrate our approach we created a little example DSML for such a robot. In the DSML the robot can

  • move forward,
  • move backwards and,
  • turn left or right.

In the following diagram the transitions between the different tasks are triggered by inputs which represent either environmental measurements or timeouts.

Model

We can simulate the execution of such a model using model transformation rules and generate code from the model that runs on the target platform, which is LEGO Mindstorms in our case study. In both cases we want to verify the correct behavior of the model using Runtime Verification. Correctness properties can be formulated in terms of the active inputs and tasks.

In the following video we demonstrate how the model transformation rules and LTL evaluation are applied on the target hardware. The robot is supposed to

  • Move forward.
  • Go back and turn left in case of an obstacle.
  • Go back and turn right if it reaches the border of the table.

The exemplary correctness property states that obstacles are static objects which do not move. In other words, if the robot goes back, the detected obstacle must be out of range again. Otherwise the obstacles comes after the robot.

Used Tools

Literature

Contact

This project is part of a research collaboration with the Bergen University College with contributions of Fernando Macias, Torben Scheffel, Malte Schmitz, Rui Wang, Martin Leucker, Adrian Rutle and Volker Stolz.