detectEr - A Runtime Monitoring tool for Erlang-Based Systems

DetectEr is a prototype academic tool that verifies correctness properties of Erlang systems at runtime. Similar to other runtime verification tools, it uses runtime information so as to mitigate state explosion problems synonymous with exhaustive formal techniques such as Model Checking. More specifically, the tool synthesises monitors (actual Erlang programs) from specifications written in a branching-time logic called the Hennessy Milner Logic with Recursion; these monitors are then instrumented to execute concurrently with a system, analysing the events it generates and flagging whenever a property satisfaction or violation is detected. The aims of the project based around detectEr are:

  1. To study issues that arise when runtime verifying concurrent and distributed systems. These are mainly engineering challenges dealing with instrumentation techniques that aim minimise the level of instrusion and overheads while still guaranteeing adequate levels of monitor observations, together with aspects that potentially lead to erroneous monitor verdicts such as race conditions.
  2. To study monitor correctness. Monitors are part of the trusted computing bases of a runtime verification setup and they are correct themselves. Yet there are many possible definitions of monitor correctness. In this project we attempt to formalise notions of monitors correctness that are close enough to actual implementations so as to incorporate aspects such as instrumentation and monitor parallelisation. We also study compositional techniques that facilitate proofs for monitor correctness.
  3. To study the expressivity of runtime verification as a technique for ensuring system correctness. We specifically chose to adopt a branching-time logic as our specification language so as to be able to determine which syntactic subsets can be verified correctly and adequately at runtime.


  1. Synthesising Correct Concurrent Runtime Monitors (Extended Abstract)
    Adrian Francalanza, Aldrin Seychell. International Conference on Runtime Verification (RV), 2013. PDF
  2. On Synchronous and Asynchronous Monitor Instrumentation for Actor-based systems
    Ian Cassar, Adrian Francalanza. FOCLASA: International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems, Rome, 2014. PDF
  3. Improving Runtime Overheads for detectEr
    Ian Cassar, Adrian Francalanza, Simon Said. International Workshop on Formal Engineering approaches to Software Components and Architectures, (FESCA) London, 2015. PDF
  4. Synthesising Correct Concurrent Runtime Monitors
    Adrian Francalanza, Aldrin Seychell. Journal of Formal Methods in System Design (FMSD), 2015. PDF
  5. Runtime Adaptation for Actor Systems
    Ian Cassar, Adrian Francalanza. International Conference on Runtime Verification (RV), 2015. PDF
  6. On Verifying Hennessy-Milner Logic with Recursion at Runtime
    Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir. International Conference on Runtime Verification (RV), 2015. PDF
  7. A Theory of Monitors
    Adrian Francalanza. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2016. PDF
  8. On Implementing a Monitor-Oriented Programming Framework for Actor Systems
    Ian Cassar, Adrian Francalanza. International Conference on integrated Formal Methods (iFM), 2016. PDF


The latest stable version is detectEr 2.0, which builds upon the foundation provided by v1.0 by allowing users to choose between the following 3 monitoring modes:

1. Asynchronous Monitoring
The monitor is a loosely-coupled process which runs in the background and observes the system without interacting with it in any way. Although monitoring is very efficient and lightweight, violations are not guaranteed to be detected immediately.
2. Synchronous Monitoring
The monitor is a tightly-coupled process which is able to temporarily block certain parts of the system so to ensure timely detection. Since the monitor and the system need to frequently interact, synchronous monitoring is less efficient than asynchronous monitoring. However, as it guarantees timely detection of violations, synchronous monitoring is ideal for monitoring safety-critical properties.
3. Hybrid Monitoring
This monitoring mode combines Asynchronous and Synchronous monitoring so to ensure timely detections with an efficiency which is very close to that of asynchronous monitoring.



The Erlang Runtime environment is required to execute the tool. It has been tested on versions R14B04 and above. It can be downloaded from the Erlang Website.


DetectEr 1.0 can be downloaded from here. The instructions on how to run the tool can be found in the README file inside the archive.

A stable version of DetectEr 2.0 can be downloaded from our bitbucket repository. The repository also has a Wiki which provides further explanation about the core concepts of the tool, as well as a detailed User Manual.

Contact details
Dr. Adrian Francalanza
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD2080,

Tel: (+356) 2340 2745
Fax: (+356) 2132 0539
Ian Cassar
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD2080,