Problem / Motivation

Motivation for running models at runtime

When designing systems one does often start with informal texts or images of situations, requierements and visions. These are often tranferred into some kind of a more or less formal model. These models are then taken by programmers and implemented using traditional programming.

Can models at runtime save work?

Every of these three steps costs effort and brings the danger of transferring information in a wrong way. Therefore it is tempting to omit one of these steps. The first step will always happen as our human brains work informally and (most of us) can not think in formal models. Starting to program without having a model has the disadvantage that non-programmers are not able to verify whether the implementation is correct. Larger amounts of source code are difficult to understand and almost impossible to verify by programmers either. So the idea is to model scenarios: Little actions that can take place and form bigger sequences of events. (Maybe even in an emergent fashion). These little scenarios should be easy to understand and therefore be easy to verifiy. Running these scenarios directly renders the programming part useless and removes the possible understanding- and implemention-errors occuring when tranferring models to code.

Is testing models at runtime easier?

A second advantage of models at runime is the possibility to quite easily check for possible livelocks or deadlocks. The reachability game is a game theoretical approach: The environment “plays” against the system and tries to do everything to bring the system into a state of safety violation while the system tries to find an accepting state (that is one, where no message has to happen next immediately)