Runtime verification of distributed systems

Abstract

Correctness verification of distributed systems poses a challenge when contrasted with monolithic systems. Due to the complexity of distributed architectures, traditional software verification techniques do not provide adequate coverage when applied over such systems, pertaining to the distributed nature of the global state. Amongst the various software verification techniques available, runtime verification is deemed a sound approach to evaluate the correctness of distributed systems. Runtime verification requires analysis of the target system's traces to evaluate the systems behaviour. In the case of distributed architectures, it proves challenging to extract a globally ordered trace, as a global clock is not available. Furthermore, distributed architecture retaining a dynamic topology may require monitors to adapt to locations unknown at runtime. Several monitoring strategies already exist to compensate for these issues. Gauci et al. proposed migrating monitors; a novel monitoring strategy for runtime verification of distributed systems. Monitors modelled over this strategy employ trace analysis locally and migrate to the respective location when requesting resources that are not available locally. This monitoring strategy, whilst reducing information exposure over communication mediums, is shown to be as effective as other monitoring approaches. Yet, an implementation of migrating monitors has never been carried out. To study this monitoring strategy, they presented an adaptation of distributed 'if-calculus, mDPI, which is expressive enough to model and reason about migrating monitors. This dissertation aims to show that the implementation of mDPI as a logic for runtime verification is achievable, and as a corollary, we show that a migrating monitor strategy is implementable for monitoring over a distributed framework. Using work in this area, a framework is designed and implemented which allows the necessary functionality to model the logic expressed in mDPI and achieve a migrating monitor strategy over a distributed setting.