↓Skip to main content

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

Verification Time Petri Nets Tina Patterns
Table of Contents

Silvano Dal Zilio, Bernard Berthomieu
In TTCS 2015 — 1st IFIP International Conference on Topics in Theoretical Computer Science, aug 2015.

conference paper

 PDF  DOI〈10.1007/978-3-319-10512-3_7〉

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.

Citation
#


@InProceedings{DalzilioS:ttcs2015probes,
   author    = {{Dal Zilio}, Silvano and Berthomieu, Bernard},
   title     = {{Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus}},
   booktitle = {TTCS 2015 -- 1st IFIP International Conference on Topics in Theoretical Computer Science},
   series    = {Lecture Notes in Computer Science},
   volume    = {9541},
   publisher = {Springer-Verlag},
   doi = {10.1007/978-3-319-10512-3_7},
   pages     = {85--99},
   month     = aug, 
   year      = 2015
}