Operational and Declarative Runtime Verification and their Combination
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 in the extreme further control a system, diverting its operation to avoid failure. One can identify two 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 is related to the previous one. 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 big picture’ view about the desired execution sequence but has complexity deficiencies when the specification includes arithmetic and data operations in general. We describe the two modes of specification, where the declarative part is based on first-order temporal logic. 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 allows benefitting from both capabilities and reducing the deficiencies of each of the separate methods.
Slides (keynotePeled.pptx) | 5.74MiB |
Thu 19 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 16:30 | Afternoon keynote 2VORTEX at EI 4 Reithoffer Chair(s): Davide Ancona DIBRIS, University of Genova, Italy | ||
15:30 60mKeynote | Operational and Declarative Runtime Verification and their Combination VORTEX K: Doron Peled Bar Ilan University, K: Klaus Havelund Jet Propulsion Laboratory, California Institute of Technology File Attached |