1. Global State Estimates for Distributed Systems
- Author
-
Thierry Massart, Tristan Le Gall, Hervé Marchand, Gabriel Kalyon, Université libre de Bruxelles (ULB), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA), Verification models and techniques applied to testing and control of reactive systems (VERTECS), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Roberto Bruni, Juergen Dingel, TC 6, WG 6.1, and Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA))
- Subjects
0209 industrial biotechnology ,Finite-state machine ,Theoretical computer science ,Reachability problem ,FIFO (computing and electronics) ,Computer science ,Informatique générale ,Subroutine ,Distributed computing ,Computation ,0102 computer and information sciences ,02 engineering and technology ,[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] ,Abstract interpretation ,01 natural sciences ,Undecidable problem ,020901 industrial engineering & automation ,010201 computation theory & mathematics ,State (computer science) ,Algorithm - Abstract
International audience; We consider distributed systems modeled as communicating finite state machines with reliable unbounded FIFO channels. As an essential sub-routine for control, monitoring and diagnosis applications, we provide an algorithm that computes, during the execution of the system, an estimate of the current global state of the distributed system for each local subsystem. This algorithm does not change the behavior of the system; each subsystem only computes and records a symbolic representation of the state estimates, and piggybacks some extra information to the messages sent to the other subsystems in order to refine their estimates. Our algorithm relies on the computation of reachable states. Since the reachability problem is undecidable in our model, we use abstract interpretation techniques to obtain regular overapproximations of the possible FIFO channel contents, and hence of the possible current global states. An implementation of this algorithm provides an empirical evaluation of our method.
- Published
- 2011