Decentralised LTL monitoring
From MaRDI portal
Publication:346789
DOI10.1007/978-3-642-32759-9_10zbMATH Open1392.68229arXiv1111.5133OpenAlexW1519460009MaRDI QIDQ346789FDOQ346789
Authors: Andreas Bauer, Yliès Falcone 
Publication date: 30 November 2016
Published in: Formal Methods in System Design, FM 2012: Formal Methods (Search for Journal in Brave)
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 an 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 satisfac- tion or violation of specifications can be detected by local monitors alone. We present an implementation and show that our algorithm introduces only a minimum delay in detecting satisfaction/violation of a specification. Moreover, our practical results show that the communication overhead introduced by the local monitors is considerably lower than the number of messages that would need to be sent to a central data collection point.
Full work available at URL: https://arxiv.org/abs/1111.5133
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- \textsc{InterAspect}: aspect-oriented instrumentation with GCC
- The complexity of propositional linear temporal logics
- Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
- Planning for temporally extended goals.
- Title not available (Why is that?)
- Timing analysis of the flexRay communication protocol
- Title not available (Why is that?)
- Decentralised LTL monitoring
- Comparing LTL semantics for runtime verification
- Rule systems for run-time monitoring: from EAGLE to RULER
- The complexity of codiagnosability for discrete event and timed systems
- Model checking of safety properties
- Diagnosis of discrete event systems using decentralized architectures
Cited In (16)
- Title not available (Why is that?)
- Decentralized LTL enforcement
- Computer says no: verdict explainability for runtime monitors using a local proof system
- Runtime enforcement with reordering, healing, and suppression
- Decentralized runtime verification of message sequences in message-based systems
- Assumption-based runtime verification
- A survey of challenges for runtime verification from advanced application domains (beyond software)
- Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation
- Monitoring metric first-order temporal properties
- Synthesising correct concurrent runtime monitors
- Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
- Decentralised LTL monitoring
- Formal analysis and offline monitoring of electronic exams
- Efficient abstraction algorithms for predicate detection
- Runtime verification of partially-synchronous distributed system
- Organising LTL monitors over distributed systems with a global clock
This page was built for publication: Decentralised LTL monitoring
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q346789)
