Ascertaining program correctness through testing is limited because it is inherently hard to cover all possible execution scenarios through finite test runs. An alternative, albeit complementing technique to testing is that of Runtime Verification, whereby a monitor program runs concurrently with the main program and performs runtime checks with respect to the main program's current execution.
Erlang is particularly suited to such a technique. Due, in part, to its lack of static checks, the language has traditionally advocated for programs that incorporate precautionary runtime checks; these defensive checks make programs resilient to unforseen circumstances not covered by the normal program logic. Moreover, Erlang's native support for concurrent processes, together with the recent advent of multicore architectures, should in theory enable the deployment of monitor programs running concurrently with the main program at a negligible runtime cost.
In this talk we advocate for a Runtime Verification approach to Erlang program development where runtime checks are teased apart from the actualy program logic, and delegated to a separate monitor program. In some sense, this is an extension of the existing link/monitor mechanism in Erlang; at present this only comes into force once a monitored process dies; through native mechanisms such as tracing and messaging, this can however be made aware of the intermediate execution of programs so as to be able to check whether this execution adheres to some specified property. This approach carries with it a number of advantages:
i) it yeilds better separation of concerns, where the main code is not cluttered with runtime checks obscuring the main program logic;
ii) it allows for the monitored properties to be specified using independent property-based logic tools. Properties written in this logic can then be synthesised automatically into an Erlang monitor process and deployed.
iii) it allows for a more modular approach to property monitoring, whereby properties monitored can be changed without affecting the main code of the program.
We evince this approach by adapting Larva, an existing tool for monitoring Java programs, to monitor Erlang program executions with respect to automata-based properties. We discuss our achievements so far and outline exciting directions for future work.