Organising LTL Monitors over Distributed Systems with a Global Clock

Christian Colombo 1 Yliès Falcone 2, 3, *
* Auteur correspondant
3 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Users wanting to monitor distributed systems often prefer to abstract away the architecture of the system by directly specifying correctness properties on the global system behaviour. To support this abstraction, a compilation of the properties would not only involve the typical choice of monitoring algorithm, but also the organisation of submonitors across the component network. Existing approaches, considered in the context of LTL properties over distributed systems with a global clock, include the so-called orchestration and migration approaches. In the orchestration approach, a central monitor receives the events from all subsystems. In the migration approach, LTL formulae transfer themselves across subsystems to gather local information. We propose a third way of organising submonitors: choreography, where monitors are organised as a tree across the distributed system, and each child feeds intermediate results to its parent. We formalise choreography-based decentralised monitoring by showing how to synthesise a network from an LTL formula, and give a decentralised monitoring algorithm working on top of an LTL network. We prove the algorithm correct and implement it in a benchmark tool. We also report on an empirical investigation comparing these three approaches on several concerns of decentralised monitoring: the delay in reaching a verdict due to communication latency, the number and size of the messages exchanged, and the number of execution steps required to reach the verdict.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2016, 49 (1-2), pp.50. 〈http://link.springer.com/article/10.1007%2Fs10703-016-0251-x〉. 〈10.1007/s10703-016-0251-x〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01315776
Contributeur : Yliès Falcone <>
Soumis le : vendredi 13 mai 2016 - 17:00:46
Dernière modification le : jeudi 11 janvier 2018 - 06:27:21
Document(s) archivé(s) le : mercredi 16 novembre 2016 - 04:40:25

Fichier

fmsd4.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Christian Colombo, Yliès Falcone. Organising LTL Monitors over Distributed Systems with a Global Clock. Formal Methods in System Design, Springer Verlag, 2016, 49 (1-2), pp.50. 〈http://link.springer.com/article/10.1007%2Fs10703-016-0251-x〉. 〈10.1007/s10703-016-0251-x〉. 〈hal-01315776〉

Partager

Métriques

Consultations de la notice

287

Téléchargements de fichiers

110