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 [40 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01666995
Contributeur : Yliès Falcone <>
Soumis le : mardi 19 décembre 2017 - 08:54:27
Dernière modification le : jeudi 11 janvier 2018 - 06:28:14

Fichier

jss.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

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〉

Partager

Métriques

Consultations de la notice

98

Téléchargements de fichiers

15