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.