Specification-based runtime verification is a technique for monitoring program executions against specifications formalized in formal logic. Such logics are usually temporal in nature, capturing the relation between events occurring at different time points. A particular challenge in runtime verification is the elegant specification and efficient monitoring of streams of events that carry data, also referred to as parametric monitoring. This paper presents two parametric runtime verification systems representing two quite different approaches to the problem. qea (Quantified Event Automata) is a state machine approach based on trace-slicing, while LogFire is a rule-based approach based on the Rete algorithm, known from AI as being the basis for many rule systems. The presentation focuses on how easy it is to specify properties in the two approaches by specifying a collection of properties gathered during the 1st International Competition of Software for Runtime Verification (CSRV 2014), affiliated with RV 2014 in Toronto, Canada.
CITATION STYLE
Havelund, K., & Reger, G. (2015). Specification of parametric monitors quantified event automata versus rule systems. In Formal Modeling and Verification of Cyber-Physical Systems: 1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015 (pp. 151–189). Springer Fachmedien. https://doi.org/10.1007/978-3-658-09994-7_6
Mendeley helps you to discover research relevant for your work.