Skip to Main content Skip to Navigation
Conference papers

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

Silvano Dal Zilio 1 Bernard Berthomieu 1
1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
LAAS - Laboratoire d'analyse et d'architecture des systèmes
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.
Complete list of metadatas
Contributor : Silvano Dal Zilio <>
Submitted on : Monday, September 21, 2015 - 4:53:31 PM
Last modification on : Thursday, March 5, 2020 - 4:28:27 PM
Document(s) archivé(s) le : Tuesday, December 29, 2015 - 9:04:41 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Silvano Dal Zilio, Bernard Berthomieu. Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus. 1st International Conference on Theoretical Computer Science (TTCS), Aug 2015, Teheran, Iran. pp.90-104, ⟨10.1007/978-3-319-28678-5_7⟩. ⟨hal-01202799⟩



Record views


Files downloads