Predictive Runtime Verification of Timed Properties

Abstract : Runtime verification (RV) techniques are used to continuously check whether the (un-trustworthy) output of a black-box system satisfies or violates a desired property. When we consider runtime verification of timed properties, physical time elapsing between actions influences the satisfiability of the property. This paper introduces predictive runtime verification of timed properties where the system is not entirely a black-box but something about its behaviour is known a priori. A priori knowledge about the behaviour of the system allows the verification monitor to foresee the satisfaction (or violation) of the monitored property. In addition to providing a conclusive verdict earlier , the verification monitor also provides additional information such as the minimum (maximum) time when the property can be violated (satisfied) in the future. The feasibility of the proposed approach is demonstrated by a prototype implementation, which is able to synthesize predictive runtime verification monitors from timed automata.
Type de document :
Article dans une revue
Journal of Systems and Software, Elsevier, 2017, 132, pp.353 - 365. 〈10.1016/j.jss.2017.06.060〉
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger
Contributeur : Yliès Falcone <>
Soumis le : mardi 19 décembre 2017 - 08:54:27
Dernière modification le : mercredi 27 février 2019 - 22:50:28


Fichiers produits par l'(les) auteur(s)



Srinivas Pinisetty, Thierry Jéron, Stavros Tripakis, Yliès Falcone, Hervé Marchand, et al.. Predictive Runtime Verification of Timed Properties. Journal of Systems and Software, Elsevier, 2017, 132, pp.353 - 365. 〈10.1016/j.jss.2017.06.060〉. 〈hal-01666995〉



Consultations de la notice


Téléchargements de fichiers