Decentralised LTL Monitoring

Andreas Bauer 1 Yliès Falcone 2, *
* Auteur correspondant
2 CORSE - Compiler Optimization and Run-time Systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Users wanting to monitor distributed or component-based systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behaviour as opposed to many components displaying many local behaviours that together constitute the system's global behaviour. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the system's global behaviour in terms of a linear-time temporal logic (LTL) formula. However, the problem that arises then is how such a specification can actually be monitored in a distributed system that has no central data collection point, where all the components' local behaviours are observable. In this case, the LTL specification needs to be decomposed into sub-formulae which, in turn, need to be distributed amongst the components' locally attached monitors, each of which sees only a distinct part of the global behaviour. The main contribution of this paper is an algorithm for distributing and monitoring LTL formulae, such that satisfaction or violation of specifications can be detected by local monitors alone. We present an implementation and show that our algorithm introduces only a negligible delay in detecting satisfaction/violation of a specification. Moreover, our practical results show that the communication overhead introduced by the local monitors is generally lower than the number of messages that would need to be sent to a central data collection point. Furthermore, our experiments strengthen the argument that the algorithm performs well in a wide range of different application contexts, given by different system/communication topologies and/or system event distributions over time.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2016, 48 (1-2), pp.48. 〈http://link.springer.com/article/10.1007%2Fs10703-016-0253-8〉. 〈10.1007/s10703-016-0253-8〉
Liste complète des métadonnées

Littérature citée [33 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01313730
Contributeur : Yliès Falcone <>
Soumis le : mardi 10 mai 2016 - 13:09:14
Dernière modification le : mercredi 11 avril 2018 - 01:59:58
Document(s) archivé(s) le : mardi 15 novembre 2016 - 23:20:23

Fichier

fmsd3-author.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Andreas Bauer, Yliès Falcone. Decentralised LTL Monitoring. Formal Methods in System Design, Springer Verlag, 2016, 48 (1-2), pp.48. 〈http://link.springer.com/article/10.1007%2Fs10703-016-0253-8〉. 〈10.1007/s10703-016-0253-8〉. 〈hal-01313730〉

Partager

Métriques

Consultations de la notice

189

Téléchargements de fichiers

143