Runtime Verification Through Forward Chaining

Alan Perotti
(University of Turin, Italy)
Guido Boella
(University of Turin, Italy)
Artur d'Avila Garcez
(City University London, UK)

In this paper we present a novel rule-based approach for Runtime Verification of FLTL properties over finite but expanding traces. Our system exploits Horn clauses in implication form and relies on a forward chaining-based monitoring algorithm. This approach avoids the branching structure and exponential complexity typical of tableaux-based formulations, creating monitors with a single state and a fixed number of rules. This allows for a fast and scalable tool for Runtime Verification: we present the technical details together with a working implementation.

In Nikolaj Bjørner, Fabio Fioravanti, Andrey Rybalchenko and Valerio Senni: Proceedings First Workshop on Horn Clauses for Verification and Synthesis (HCVS 2014), Vienna, Austria, 17 July 2014, Electronic Proceedings in Theoretical Computer Science 169, pp. 68–81.
Published: 2nd December 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: