Combining testing and runtime verification techniques

Abstract

Testing is an established and integral part of the system design and development process, but incomplete coverage still leaves room for potential undiscovered bugs. Runtime verification addresses this issue by integrating verification

oracles into the code, allowing for reparatory action to be taken in case of system failure after deployment. Despite the complementarity of the two approaches,

the application of the two approaches at different stages in the development and

deployment process results in much duplication of effort. In this paper we investigate the combination of the two approaches, by showing how one can use testing

oracles to derive correct runtime verification monitors. We show how this can be achieved using QuickCheck and Larva, and apply the resulting framework to Riak, a fault-tolerant distributed database written in Erlang.