Operational and Declarative Runtime Verification (Keynote)

Runtime verification (RV) is used to monitor the execution of a system and check it against a formal specification. It can detect failures, and can also be used to control a system, diverting its operation to avoid failure. One can identify two main approaches of specifying properties to be monitored: {\em operational specification} and {\em declarative specification}. Operational specification describes, using a programming language like formalism, how each new monitored event updates a program state consisting of user defined variables. This kind of specification is attractive for describing aggregated arithmetic calculations and can be implemented with a very simple RV algorithm. Declarative specification describes whether the sequence of inputs satisfies a propositional or first-order temporal property. This kind of specification gives a global view about the desired execution sequence but has complexity deficiencies when the specification includes arithmetic and data operations in general. We describe an RV system designed and implemented to work with the two kinds of specifications. It allows ongoing results to be sent between the two parts. This results in benefiting from both capabilities and reducing the deficiencies of each of the separate methods. We compare with an alternative approach implementing a logic as an internal DSL in a programming language and with a mixed approach that allows importing a declarative RV component in a program written in a programming language.