%0 Conference Proceedings
%T Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus
%+ Équipe Verification de Systèmes Temporisés Critiques (LAAS-VERTICS)
%A Dal Zilio, Silvano
%A Berthomieu, Bernard
%Z This work was presented at TTCS 2015, the First IFIP International Conference on Topics in Theoretical Computer Science, August 26-28,2015. Institute for Research in Fundamental Sciences (IPM), Tehran, Iran.
%< avec comité de lecture
%Z Rapport LAAS n° 15356
%( Lecture Notes in Computer Science
%B 1st International Conference on Theoretical Computer Science (TTCS)
%C Teheran, Iran
%Y Mohammad Taghi Hajiaghayi
%Y Mohammad Reza Mousavi
%I Springer
%3 Topics in Theoretical Computer Science
%V LNCS-9541
%P 90-104
%8 2015-08-26
%D 2015
%Z 1509.06507
%R 10.1007/978-3-319-28678-5_7
%K real time model checking
%K time Petri nets
%Z Computer Science [cs]/Embedded Systems
%Z Computer Science [cs]/Logic in Computer Science [cs.LO]Conference papers
%X 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.
%G English
%Z TC 1
%Z WG 1.8
%2 https://hal.science/hal-01202799/document
%2 https://hal.science/hal-01202799/file/article.pdf
%L hal-01202799
%U https://hal.science/hal-01202799
%~ UNIV-TLSE2
%~ UNIV-TLSE3
%~ CNRS
%~ INSA-TOULOUSE
%~ LAAS
%~ OPENAIRE
%~ UT1-CAPITOLE
%~ IFIP-LNCS
%~ IFIP
%~ LAAS-VERTICS
%~ LAAS-INFORMATIQUE-CRITIQUE
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG
%~ IFIP-LNCS-9541
%~ IFIP-WG1-8
%~ IFIP-TTCS
%~ INSA-GROUPE
%~ LAAS-RISC
%~ TOULOUSE-INP
%~ UNIV-UT3
%~ UT3-INP
%~ UT3-TOULOUSEINP
%~ TEST7-HALCNRS