Specification of parametric monitors quantified event automata versus rule systems

Klaus Havelund, Giles Reger

    Research output: Chapter in Book/Report/Conference proceedingChapter

    Abstract

    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.

    Original languageEnglish
    Title of host publicationFormal 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
    PublisherSpringer Nature
    Pages151-189
    Number of pages39
    ISBN (Print)9783658099947, 9783658099930
    DOIs
    Publication statusPublished - 5 Jun 2015

    Fingerprint

    Dive into the research topics of 'Specification of parametric monitors quantified event automata versus rule systems'. Together they form a unique fingerprint.

    Cite this