polyLARVA plugin for Erlang

Abstract

Runtime verification is a technique used to verify the correctness of software behaviour at run-time as described in a formal specification. In general this requires the concept of system events, which means that a system running under runtime verification must fire system events during execution which exist for the purpose of making the system behaviour detectable. Additionally a runtime verification tool may also execute actions on a monitored system normally upon the detection of incorrect behaviour. These requirements suggest that a runtime verification tool cannot be entirely independent of the programming language used to implement a system to be monitored. polyLARVA is a runtime verification framework which is designed to support multiple programming languages by separating generic functionality from the functionality that is specific to a particular language. This is achieved by creating a remote-side monitor and a system-side monitor where the remote-side is completely independent of the programming language of the monitored system while the system-side monitor is specific to a particular language. In this work, polyLARVA is extended to support the Erlang language. This involved defining an appropriate specification to define behaviour of Erlang programs and using this specification to generate a system-side monitor for Erlang which is incorporated into the system using aspect-oriented programming techniques. The generated monitor detects Erlang events and communicates with a remote-side monitor to check for correctness accordingly. The resulting artifact is used to monitor Riak, an open-source database written in Erlang, such as to determine the effectiveness of the solution on a real-world example. Riak's implementation is investigated in depth to define aspects of its behaviour and monitor them to determine to the usefulness of the artifact.