Operational and Declarative Runtime Verification (Keynote)

Runtime verification (RV) is used to monitor executions of a system, checking them against a formal specification. It can detect failures, and can also be used to control a system, diverting its operation to avoid a failure. One can identify two main approaches of specifying properties to be monitored: operational specification and declarative specification. Operational specification describes, using a programming language like formalism, how each new monitored event updates a summary of the observed sequence of events, consisting of user defined variables. This kind of specification is attractive, e.g., for describing aggregated arithmetic calculations and can be very simple to implement. Declarative specification gives a more global view of the requirements that the monitored execution sequences must satisfy, based on a temporal formalism, e.g., propositional or first-order temporal logic. We describe an RV system designed and implemented to work with the two kinds of specifications. It allows the two parts to collaborate by sending ongoing results between them. This results in benefiting from both capabilities and reducing the deficiencies of each of the separate specification methods. We compare alternative approaches to combining operational and declarative specification as internal and external DSLs.