Assumption-based Runtime Verification

Abstract

Runtime Verification is a lightweight automatic verification technique. We introduce Assumption-Based Runtime Verification framework, which is capable for monitoring partially observable systems. The framework leverages assumptions on the behaviors of the systems under scrutiny for reasoning on their the non-observable or future behaviors. The specification is expressed in Propositional Linear Temporal Logic (LTL) with both future and past temporal operators, while assumptions are described in Fair Kripke Structures. Static or dynamic sets of observables are supported. The monitors are also resettable, i.e. being able to evaluate the specification at arbitrary positions of the input trace. We present the formalism of the framework and a series of monitoring algorithms which can be efficiently implemented by Binary Decision Diagrams. As a by-product, we also present a new automata-based monitor construction for Past-time LTL, an LTL variant with only past temporal operators. We give proofs for the correctness of all involved algorithms. The framework is implemented in NuRV, an extension of the nuXmv model checker. It synthesizes implicit or explicit monitors which can be deployed in online or offline modes. The explicit monitors are embeddable code in programming languages including C, C++, Java and Common Lisp. In particular, monitors can be generated as SMV models, whose correctness and other properties can be verified in nuXmv. Using a benchmark from Dwyer’s LTL patterns, we show the efficiency of the symbolic approach and the generated monitors, and the feasibility and effectiveness of the approach. Some monitors are shown to be predictive under certain assumptions.