DecentMon

An OCaml Benchmark for Decentralized Monitoring

DecenMon is an OCaml Benchmark for Decentralized Monitoring of LTL formulae. DcentMont is written in the functional programming language OCaml.

DecentMon inputs and outputs

DecentMon takes as input:

  • some LTL formulae to be monitored or some LTL Specification patterns (see the Specification Patterns Website);
  • some traces against the formulae are monitored; an architecture given by a distributed alphabet indicating how components are organised and distributed in the system.

The iterations of DecentMon served producing experimental results for several publications: (Bauer & Falcone, 2012) (Bauer & Falcone, 2016) (Colombo & Falcone, 2014) (Colombo & Falcone, 2016) (Visconti et al., 2024)

Link to the repo.

References

2024

  1. Adaptable Configuration of Decentralized Monitors
    Ennio Visconti, Ezio Bartocci, Yliès Falcone, and Laura Nenzi
    In Formal Techniques for Distributed Objects, Components, and Systems - 44th IFIP WG 6.1 International Conference, FORTE 2024, Held as Part of the 19th International Federated Conference on Distributed Computing Techniques, DisCoTec 2024, Groningen, The Netherlands, June 17-21, 2024, Proceedings, 2024
    DOI

2016

  1. Decentralised LTL monitoring
    Andreas Bauer, and Yliès Falcone
    Formal Methods Syst. Des., 2016
    DOI
  2. Organising LTL monitors over distributed systems with a global clock
    Christian Colombo, and Yliès Falcone
    Formal Methods Syst. Des., 2016
    DOI

2014

  1. Organising LTL Monitors over Distributed Systems with a Global Clock
    Christian Colombo, and Yliès Falcone
    In Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, 2014
    DOI

2012

  1. Decentralised LTL Monitoring
    Andreas Klaus Bauer, and Yliès Falcone
    In FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, 2012
    DOI