Please use this identifier to cite or link to this item:
Title: Organising LTL monitors over distributed systems with a global clock
Authors: Colombo, Christian
Falcone, Ylies
Keywords: Autonomous distributed systems
Distributed algorithms
Communication models
Computer systems -- Verification
Computer algorithms
Issue Date: 2016
Publisher: Springer New York LLC
Citation: Colombo, C., & Falcone, Y. (2016). Organising LTL monitors over distributed systems with a global clock. Formal Methods in System Design, 49(1-2), 109-158.
Abstract: Users wanting to monitor distributed systems often prefer to abstract away the architecture of the system, allowing them to directly specify 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 orgnized as a tree across the distributed system, and each child feeds intermediate results to its parent. We formalise this approach, proving its correctness and worst case performance, and report on an empirical investigation comparing the three approaches on several concerns of decentralised monitoring.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Organising_LTL_monitors_over_distributed_systems_with_a_global_clock.pdf282.31 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.