Abductive runtime verification of Lustre programs

Abstract

Fully automating the process of verifying a system is fraught with complexity, in spite of significant progress in this area, and does not necessarily lead to understanding the nature of perceived faults. We present an approach to automate diagnosing a system by subjecting the system to passive monitoring, part of a technique called runtime verification. Being a partial technique, we justify its use by its potential to glean information about faults once they arise in monitored programs. Abductive runtime verification can derive additional benefit from this context by inferring possible causes of deviation from the expected program behaviour. Our approach enables observed faults to be mapped to elements in the program's code from which they arose. Moreover, the fault's symptoms are elaborated into an explanation and possible causes are suggested by a diagnostic engine. This benefits from knowledge about the structure and state of the running program to generate program slices for individual symptoms. Finally, a representation of these slices is produced in a graph language for visualisation. These artifacts are intended to provide the user with select information to assist them in focussing on the relevant parts of a program following an observed failure. In the course of the project we have explored ideas from Artificial Intelligence and Formal Methods and incorporated techniques from both fields to implement an abductive runtime verification tool for programs written in Lustre, a synchronous programming language.