We use the existing UPPAAL Model Checker, specifically its Statistical Model Checking (SMC) component, to create and verify the models for our radiation therapy application. UPPAAL uses Networks of Timed Automata (NTA) to describe systems and by the network approach can describe the relations of multiple smaller systems that together create complexity. The properties of these models can then be queried using a custom variation of TCTL formulas.

UPPAAL itself is not made to be used in an online environment. As it is common for model checkers, the intention is to provide the best possible answer to a query and guarantee the delivered results.Time is not the primary concern in that scenario, because a system is commonly verified before it is put in use.
Thus, we must intrument UPPAAL to work online ourselves.

Online Checking with UPPAAL

While we can and do prepare our models and queries such that they usually are quick to solve, this is not by itself sufficient. If we cannot check a query and use its result within a short time period, we have no use for the result. Thus, we use process control mechanisms to control the execution of UPPAAL processes and stop checks that take too long.This also allows us to check for multiple different queries in parallel instead of one at a time. Further, we can schedule our queries in a way that more important queries are checked first.

The other part is the templating of new model instances. Here, we reuse an existing software component from our institute. This component needs to be tightly integrated to fit within the online timing constraints, as the timeslot needs to fit both the model creation and the checking that then guides the application's procedure.