Runtime verification and compensations

Abstract

As systems grow more complex, it becomes increasingly difficult to ensure their correctness. One approach for added assurance is to monitor a system's execution so that if a specification violation occurs, it is detected and potentially rectified at runtime. Known as runtime verification, this technique has been gaining popularity with its main drawback being that it uses system resources to perform the checking. An effective way of minimising the intrusiveness of runtime verification is to desynchronise the system from the monitor, meaning that the system and the monitor progress independently. The problem with this approach is that the monitor may fall significantly behind the system and by the time the monitor detects a violation, it might be too late to make a correction. To tackle this issue we propose a monitoring architecture, cLARVA, providing fine control over the system-monitor relationship, enabling the monitor to be synchronised to the system by fast-forwarding through monitoring states, and the system to synchronise with the monitor by reverting it to an earlier state. Going back through system states is generally hard to automate since not all actions are reversible; reverse actions may expire, the reverse of an action may be context-dependent and so on. This subject, known as compensations, has been studied in the context of transactions where the reversal of incomplete transactions is used to ensure that either the transaction succeeds completely or it leaves no effect on the system. Although a lot of work has been done on compensations, the literature still presents challenges to compensation programming. We show how these limitations can be alleviated by separating compensation programming concerns from other concerns. Inspired by monitor-oriented programming - a way of using runtime verification to trigger functionality - we propose a novel monitor-oriented notation, compensating automata, for compensation programming. Integrated within a monitoring framework which we call monitor-oriented compensation programming, this notation enables a programmer to program and trigger compensation execution completely through monitoring with the system being unaware of compensations. Finally, we show how compensating automata can be used for programming the synchronisation between the system and the monitor in cLARVA, enabling complex compensation logic to be seamlessly programmed. To evaluate our approach, we applied it to an industrial case study based on a financial system handling virtual credit cards, consisting of thousands of users and transactions. The results show that the architecture has been successful in both synchronising the monitor to the system by fast-forwarding the monitor, and also in synchronising the system to the monitor using compensations to reverse the system state - achieving a virtually non-intrusive runtime monitoring architecture.