Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus

TL;DR

This paper presents an automated method for verifying the correctness of realtime observers in model-checking, ensuring they detect property violations without interfering with the system, implemented in the Tina tool for Time Petri Nets.

Contribution

It introduces an automated approach for testing observer correctness in realtime systems, combining visual verification with model-checking techniques.

Findings

Successfully implemented in Tina for Time Petri Nets

Automates the verification of observer correctness

Ensures observers detect violations without system interference

Abstract

A classical method for model-checking timed properties-such as those expressed using timed extensions of temporal logic-is to rely on the use of observers. In this context, a major problem is to prove the correctness of observers. Essentially, this boils down to proving that: (1) every trace that contradicts a property can be detected by the observer; but also that (2) the observer is innocuous, meaning that it cannot interfere with the system under observation. In this paper, we describe a method for automatically testing the correctness of realtime observers. This method is obtained by automating an approach often referred to as visual verification, in which the correctness of a system is performed by inspecting a graphical representation of its state space. Our approach has been implemented on the tool Tina, a model-checking toolbox for Time Petri Net.