Synchronous and asynchronous monitoring in Elarva

Abstract

ELARVA is a runtime verification (RV) framework for Erlang, a tool with which a system may be verified for correctness by continuously checking the system while it is executing. In order to carry out its function, ELARVA must somehow instrument a system such that certain events of interest are communicated with the system's monitors, processes generated by ELARVA and responsible for performing system verification. Currently, ELARVA accomplishes this using Erlang's tracing mechanism which can only generate events asynchronously, allowing the process generating the event to continue execution after event generation without any kind of synchronization with other processes (like, for example, ELARVA's monitors). Unfortunately, although asynchronous event generation is more efficient than its synchronous counterpart, when a property violation is detected by a monitor at runtime, synchronous communication between the system and its monitors becomes essential if the monitor detecting the violation is to stand any reasonable chance of restoring the system's integrity before allowing it to continue execution beyond the point at which the event was generated. This is so because synchronous event generation will stop the system's execution at the exact point at which a system property may have been broken. The generated event might result in a monitor detecting some kind of property violation, at which point, the monitor may execute preprogrammed instructions to remedy the situation before allowing the system to continue. Unlike the case when the system is allowed to continue execution before carrying out verification, these preprogrammed instructions can take advantage of the fact that the system has not continued execution after the event was generated, restricting the cause of system invalidity to that of breaking a single, known system property. Therefore, synchronous event generation is desirable and even essential when ELARVA is used to verify a system which demands the ability to recuperate from property violations. It is the objective of this FYP to explore how to go about implementing such a synchronous and asynchronous event generation mechanism for ELARVA. The intention is to provide some evidence for the adoption of certain design decisions when implementing such an artifact.