Monitoring Distributed Systems with Distributed PolyLarva

Authors: Ian Cassar, Christian Colombo, Adrian Francalanza

Corresponding: Ian Cassar (ian.cassar.10@um.edu.mt)

Keywords: none

Doi: http://dx.medra.org/10.7423/XJENZA.2014.2.05

Issue: Xjenza Online Vol. 2 Iss. 2 - October 2014

Abstract:
PolyLarva is a language-agnostic runtime verication tool, which converts a PolyLarvaScript into a monitor for a given system. While an implementa- tion for PolyLarva exists, the language and its com- pilation have not been formalised. We therefore present a formal implementation-independent model which de- scribes the behaviour of PolyLarvaScript, comprising of the LarvaScript grammar and of a set of operational semantics. This allows us to prove important proper- ties, such as determinism, and also enables us to reason about ways of re-designing the tool in a more scalable way. We also present a collection of denotational map- pings for LarvaScript converting the constructs of our grammar into constructs of a formal actor-based model, thus providing an Actor semantics for LarvaScript. We are also able to prove certain correctness properties of the denotational translation such as that the denoted Actors behave in a way which corresponds to the behaviour de- scribed by our implementation-independent model. We nally present DistPolyLarva, a prototype implementa- tion of the distributed PolyLarva tool, which implements the new actor-based semantics over a language that can na- tively handle distribution and concurrency called Erlang.

Download Article: