The online model-checking approach was proposed as a method to apply model checking to systems where accurate long-term models are difficult to obtain.

Instead of statically proving the safety of a system before the system is deployed, online model checking (OMC) is a dynamic technique that monitors the system while it is running. Periodically OMC performs a classic model-checking analysis to obtain guarantees on the current system state and its near future.

When the analyses are scheduled such that the validity scopes of the guarantees overlap, one obtains safety guarantees for the complete execution of the system. As a result if a problem arises a grace period that allows timely counter-measures is always available to ensure safe operation. The benefit of this approach is that at the verification seams the simulated state or the model itself can be modified.

When done correctly such adjustments can ensure that the used model represents the real-world system correctly even though the model is of approximate nature only.

We have developed a framework for the development of such online model-checking applications with UPPAAL. The framework lets the user define an OMC application by specifying the verification properties, the verification intervals, the adjustments for the simulation state and model, and the sensors that obtain data from the real world. The model for the system itself is still created in UPPAAL.

This approach allows the reuse of older UPPAAL models and decouples system modeling from the OMC implementation. When everything is specified the framework works fully automatic: after the start of the system the UPPAAL model is simulated synchronously to the real-world system and after every verification interval an adjustment process followed by a verification is initiated. During the adjustment process the sensor data is evaluated as specified by the user and state and model adjustments are performed. This phase requires the reconstruction of the previous state space to obtain seamless transitions and to perform the modifications. The framework provides automatic algorithms for this state space reconstruction. In the subsequent verification step the new model is subject to a model-checking analysis with the user-defined properties. If the verification fails at any point an alarm is raised and counter-measures can be performed.

The framework can be downloaded here.

References

• Jonas Rinast, Sibylle Schupp, and Dieter Gollmann. A Graph-Based Transformation Reduction to Reach UPPAAL States Faster. In Cliff Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 547–562. Springer International Publishing, 2014
• Jonas Rinast, Sibylle Schupp, and Dieter Gollmann. State Space Reconstruction in UPPAAL: An Algorithm and its Proof. International Journal On Advances in Systems and Measurements, 7(1-2):91–102, 2014
• Xintao Ma, Jonas Rinast, Sibylle Schupp, and Dieter Gollmann. Evaluating On-line Model Checking in UPPAAL-SMC using a Laser Tracheotomy Case Study. In Volker Turau, Marta Kwiatkowska, Rahul Mangharam, and Christoph Weyer, editors, 5th Workshop on Medical Cyber-Physical Systems, volume 36 of OpenAccess Series in Informatics (OASIcs), pages 100–112. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2014
• Jonas Rinast, Sibylle Schupp, and Dieter Gollmann. State Space Reconstruction for On-Line Model Checking with UPPAAL. In VALID 2013, The Fifth International Conference on Advances in System Testing and Validation Lifecycle, pages 21–26. IARIA, 2013