Skip to Main content Skip to Navigation
Journal articles

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.
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download
Contributor : Yliès Falcone Connect in order to contact the contributor
Submitted on : Tuesday, December 19, 2017 - 8:54:27 AM
Last modification on : Sunday, June 26, 2022 - 5:04:41 AM


Files produced by the author(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⟩



Record views


Files downloads