|
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:
- 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.
- 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.
- 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.
|
Papers
- Synthesising Correct Concurrent Runtime Monitors (Extended Abstract) Adrian Francalanza, Aldrin Seychell. International Conference on Runtime Verification (RV), 2013. PDF
- 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
- 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
- Synthesising Correct Concurrent Runtime Monitors Adrian Francalanza, Aldrin Seychell. Journal of Formal Methods in System Design (FMSD), 2015. PDF
- Runtime Adaptation for Actor Systems
Ian Cassar, Adrian Francalanza. International Conference on Runtime Verification (RV), 2015. PDF
- On Verifying Hennessy-Milner Logic with Recursion at Runtime
Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir. International Conference on Runtime Verification (RV), 2015. PDF
- A Theory of Monitors
Adrian Francalanza. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2016. PDF
- On Implementing a Monitor-Oriented Programming Framework for Actor Systems
Ian Cassar, Adrian Francalanza. International Conference on integrated Formal Methods (iFM), 2016. PDF
|
Tool
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.
|
|