Monitoring distributed systems with distributed PoLYLARVA

Abstract

Runtime Verification (RV) [3] is a dynamic verification technique which verifies that a system is currently executing correctly with respect to a formal specification. Since RV tools are responsible for verifying the correctness of other systems, it is important that such RV tools should be verified for correctness themselves, thus making users more confident in trusting and relying on such RV tools for the necessary system verification. As RV tools weave additional monitoring code into the system being verified, an inevitable runtime overhead is imposed upon the system. Moreover, monitoring demands may rapidly increase especially when monitoring distributed systems, since these systems are able to rapidly scale up. Such a drastic increase in monitoring load would impose a negative effect on the monitoring efficiency, thus also affecting the performance of the monitored system. For this reason, various ways are being explored by which this runtime overhead can be kept to a minimum. Concurrency and parallelisation provide a way of decreasing these monitoring overheads by exploiting tightly-coupled, multicore architectures predominant to most computers nowadays. However, when dealing with high monitoring demands, distributed monitoring may also be a scalable and more feasible alternative for increasing monitor efficiency. In this project we present a formal implementation-independent Front-End model describing the behaviour of poly-LarvaScript, the specification language of an existing runtime verification tool called PoLYLARvA [25]. This formal model, comprising of the µLarvaScript calculus and of a set of operational semantics, allows us to prove important properties, such as determinism, about the specification language. Moreover, it also enables us to reason about ways of re-designing the tool in a more scalable way which provides better support for distribution. Hence we also present a collection of denotational semantic mappings which convert the constructs of our µLarvaScript calculus into constructs of a formal actor-based, distributed Back-End model, thus providing Actor semantics for µLarvaScript. We then guarantee the correctness of the denotational mapping by proving that the denoted Actors behave in a way which corresponds to the behaviour described by our Front-End model. We finally present DisTPOLYLARVA, a prototype implementation of the distributed PoLYLARVA tool, which implements the new actor-based semantics over Erlang, a framework that can natively handle distribution and concurrency. Although the DrsTPoLYLARVA prototype provides nearly all features pertaining to the original PoLYLARVA compiler, our DisTPOLYLARvA compiler is only guaranteed to synthesise correctly behaving monitors when the given specification only includes constructs which are formalized in our µLarvaScript calculus.