Counter example shrinking for ELARVA

Abstract

Concurrent programs are usually non-deterministic, meaning that typical approaches for verifying the correctness of such programs may not always be effective. For ex ample, software testing may not unearth subtle bugs that arise only at a particular process interleaving. On the other hand, runtime verification systems can be used to ensure that a number of properties are preserved at a post-deployment stage. ELARVA is a runtime verification tool developed in Erlang which has already been successfully used in order to monitor concurrent software systems. The main issue now is, what happens when one of the properties being monitored is broken. At this point a software developer will attempt to determine what caused the system to fail. However considering the fact that a runtime verification system may have been running with no properties being violated for an extended period of time, attempting to manually understand the entire trace log becomes a very complex task. A similar problem was tackled by using shrinking techniques in order to simplify failing inputs in software testing. In this report we propose an extension to ELARVA that adds trace shrinking functionality. Whenever ELARVA detects a violation during runtime, the trace shrinking functionality will be used in order to provide a much smaller trace that produces the same violation. This smaller trace should make it easier for somebody trying to understand why the violation occurred. The main problem with applying shrinking techniques to runtime verification is that shrinking techniques require a failure to be repeatable. In order to reproduce a failure in runtime verification a replay system had to be designed which records all of the system's interactions with outside elements (like users and external libraries) during runtime. These interactions can then be replayed during the shrinking process in order to simulate the system's behaviour and determine whether a shrunk trace leads to the same violation or not. In conjunction with this replay system, algorithms like delta debugging minimization were implemented in order to systematically reduce the size of a failure trace. Tests using two different case studies confirmed that the trace shrinking extension for ELARVA successfully shrunk the execution trace after a failure had been detected through runtime verification.