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 metadatas

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/hal-01666995
Contributor : Yliès Falcone <>
Submitted on : Tuesday, December 19, 2017 - 8:54:27 AM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM

File

jss.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

1224

Files downloads

223