STS: Online Model Checking

STS > Research > Model Checking & Abstract Interpretation > Online Model Checking

Online Model Checking

Online Model Checking combines the formal modeling qualities and guarantees of Model Checking with an online (i.e. live changing) environment. A Model Checking tool requires its user to provide a model of the system in question and then is able to answer queries about the behaviour of that system.

The transfer to an online environment requires us to create derived models that represent the current state of that online system. Here, the original model is used as a template, in which data parameters are configured with current data (e.g. as received from sensors). These data parameters are an additional feature of model checkers (here, UPPAAL) beyond the formal definition of the modeling framework.

Creating a model that sufficiently captures the real world, but simplifies enough to make it comprehendable to a computer is a challenge in itself. The online setting requires models to be simple enough to allow the computer to answer queries fast before the model becomes outdated and is superseded.

Example

This graphic depicts model of human respiratory motion in its primary movement axis. It is modeled using Networks of Timed Automata (NTA) and produces a sine wave according to sensory data and introduces some randomzied variations.

We use this model in our robotic radiation therapy scenario application, which demands that a safe distance is kept from the patient at all times. Thus, we query this model for distances within a certain time window.
The model and queries are intentionally kept very simple to make it possible to answer as many queries as possible within a short time period. At the end of this period, a decision for the procedure is made based on the query results and the process begins anew by creating a new model instance with updated sensor information.
Have a look at the doctoral thesis An online model-checking framework for timed automata by Jonas Rinast.

Model Checker

We reuse the existing and established model checker UPPAAL. However, UPPAAL itself is not an online tool. In fact, commonly used model checkers are not intended for online use, but rather use as much time as necessary to provide a maximally guaranteed answer. Using specially crafted models for the purpose helps to reduce time consumption.
Further, our application uses the Statistical Model Checking (SMC) component that provides probabilities when checking rather than only guarantees, which makes sense in this kind of environment.

However, by design of model checkers it is not possible to guarantee a certain execution time window. Thus, we interact with the model checker using various process control interfaces that allow us to externally limit the tool. We can then collect the information that was possible to extract within the timeslot and produce a decision based on that information. We can also prioritize between different queries to ensure we get required results, e.g. if we can simply continue with the current procedure.

OMC software

For the online templating of sensor data into models, we also reuse an existing software component from our institute. It is designed to receive the sensor information continuesly and calculate the required data entry fields from it. It then templates the model and checks with a model checker query that it does indeed is able to predict the sensor output within a short time period.
Have at look at the OMC software component.

If you want to checkout the model for yourself, have a look at our MARS repository entry.
You can open it using the latest 4.1.x version of UPPAAL.

TU Hamburg

Institute for Software Systems (E-16)

Am Schwarzenberg-Campus 3 (E)

21073 Hamburg

E-mail : sts-office@tuhh.de

Phone : 040-42878-3460

More

Online Model Checking

Example

Model Checker

OMC software

TU Hamburg

Links