Christian Colombo
Creator of the monitoring tool Larva
University of Malta
Christian is an assistant lecturer and a PhD student at the University of Malta with a number of published papers in the area of runtime verification. In his research, he has developed a monitoring tool called Larva and applied it to an industrial Java system handling financial transactions. Currently, he is coordinating a national research project on applying monitoring techniques to industrial financial systems having compensating transactions. He recently discovered that Erlang, together with its concurrency model, lends itself well to a monitored style of programming and is now developing tools to enable and automate monitor instrumentation in Erlang. He is very excited to share these new developments at London's Erlang Factory.
Christian's Research
Christian's Research
Christian Colombo is Giving the Following Talks
Erlang -a monitoring-oriented programming language
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.
You can view Christian's slides here.
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.
You can view Christian's slides here.