DecentMon is an open-source OCaml benchmark for Decentralised LTL monitoring.
DecenMon simulates the verfication of LTL formulae at runtime on a distributed system in a decentralised fashion.
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.
One can consult this website for more information on DecentMon.