Runtime Verification in Distributed Computing

Runtime verification aims to check whether an application executes its behaviour as specified. Thereby the active execution trace of an application is checked in terms of the actual execution context; diagnosis and, possibly, recovery actions are taken when the specification is violated. In today’s practices, software is increasingly distributed over multiple processes, potentially running at different locations. This is supported by middleware that, to some extent, allows implementing applications in a distribution-transparent way. To enable effective runtime verification in distributed software we focus in this paper on three requirements: (1) distribution-transparent specification of software behaviour, as software is also implemented in such a way, (2) end-to-end verification of behaviour, and (3) automatic generation of verification modules for arbitrary process and distribution structures. We present a novel runtime verification approach satisfying these requirements and present its implementation in the EventChaser system. Furthermore we present an approach that at least minimizes the distribution-awareness of specifications to an acceptable level for software not using supported middleware for inter-process communication