Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berry, G., Gonthier, G.: The esterel synchronous programming language: Design, semantics, implementation. Sci. Comput. Program. 19(2), 87–152 (1992)
Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 172–186. Springer, Heidelberg (1997)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
Cassandras, C., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)
Chatain, T., Gastin, P., Sznajder, N.: Natural specifications yield decidability for distributed synthesis of asynchronous systems. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 141–152. Springer, Heidelberg (2009)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252 (1977)
Debouk, R., Lafortune, S., Teneketzis, D.: Coordinated decentralized protocols for failure diagnosis of discrete event systems. Discrete Event Dynamical Systems: Theory and Applications 10, 33–79 (2000)
Genest, B.: On implementation of global concurrent systems with local asynchronous controllers. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 443–457. Springer, Heidelberg (2005)
Hélouet, L., Gazagnaire, T., Genest, B.: Diagnosis from scenarios. In: Proc. of the 8th Int. Workshop on Discrete Events Systems, WODES 2006, pp. 307–312 (2006)
Heußner, A., Le Gall, T., Sutre, G.: Extrapolation-based path invariants for abstraction refinement of fifo systems. In: Păsăreanu, C.S. (ed.) Model Checking Software. LNCS, vol. 5578, pp. 107–124. Springer, Heidelberg (2009)
Kalyon, G., Le Gall, T., Marchand, H., Massart, T.: Global state estimates for distributed systems (version with proofs). In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE 2011. LNCS, vol. 6722, pp. 194–203. Springer, Heidelberg (2011), http://hal.inria.fr/inria-00581259/
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–565 (1978)
Le Gall, T., Jeannet, B., Jéron, T.: Verification of communication protocols using abstract interpretation of FIFO queues. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 204–219. Springer, Heidelberg (2006)
Lin, F., Rudie, K., Lafortune, S.: Minimal communication for essential transitions in a distributed discrete-event system. Trans. on Automatic Control 52(8), 1495–1502 (2007)
Massart, T.: A calculus to define correct tranformations of lotos specifications. In: FORTE 1991. IFIP Transactions, vol. C-2, pp. 281–296 (1991)
Mattern, F.: Virtual time and global states of distributed systems. In: Proceedings of the Workshop on Parallel and Distributed Algorithms, pp. 215–226 (1989)
The McScM library (2009), http://altarica.labri.fr/forge/projects/mcscm/wiki/
Ricker, L., Caillaud, B.: Mind the gap: Expanding communication options in decentralized discrete-event control. In: Conference on Decision and Control (2007)
Sampath, M., Sengupta, R., Lafortune, S., Sinaamohideen, K., Teneketzis, D.: Failure diagnosis using discrete event models. IEEE Transactions on Control Systems Technology 4(2), 105–124 (1996)
Tripakis, S.: Decentralized control of discrete event systems with bounded or unbounded delay communication. IEEE Trans. on Automatic Control 49(9), 1489–1501 (2004)
Xu, S., Kumar, R.: Distributed state estimation in discrete event systems. In: ACC 2009: Proc. of the 2009 conference on American Control Conference, pp. 4735–4740 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kalyon, G., Le Gall, T., Marchand, H., Massart, T. (2011). Global State Estimates for Distributed Systems. In: Bruni, R., Dingel, J. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2011 2011. Lecture Notes in Computer Science, vol 6722. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21461-5_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-21461-5_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21460-8
Online ISBN: 978-3-642-21461-5
eBook Packages: Computer ScienceComputer Science (R0)