Skip to main content

Monitoring Distributed Systems Using Knowledge

  • Conference paper
Formal Techniques for Distributed Systems (FMOODS 2011, FORTE 2011)

Abstract

In this paper, we use knowledge-based control theory to monitor global properties in a distributed system. We control the system to enforce that if a given global property is violated, at least one process knows this fact, and therefore may report it. Our approach uses knowledge properties that are precalculated based on model checking. As local knowledge is not always sufficient to monitor a global property in a concurrent system, we allow adding temporary synchronizations between two or more processes to achieve sufficient knowledge. Since synchronizations are expensive, we aim at minimizing their number using the knowledge analysis.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K., Francez, N.: Modeling the Distributed Termination Convention of CSP. ACM Trans. Program. Lang. Syst. 6(3), 370–379 (1984)

    Article  MATH  Google Scholar 

  2. Basu, A., Bensalem, S., Peled, D., Sifakis, J.: Priority Scheduling of Distributed Systems based on Model Checking. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 79–93. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Bensalem, S., Bozga, M., Graf, S., Peled, D., Quinton, S.: Methods for Knowledge Based Controlling of Distributed Systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 52–66. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Chandy, K., Lamport, L.: Distributed Snapshots: Determining Global States of Distributed Systems. ACM Trans. Comput. Syst. 3(1), 63–75 (1985)

    Article  Google Scholar 

  5. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)

    MATH  Google Scholar 

  6. Genrich, H.J., Lautenbauch, K.: System Modeling with High-level Petri Nets. Theoretical Computer Science 13, 109–135 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  7. Graf, S., Peled, D., Quinton, S.: Achieving Distributed Control through Model Checking. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 396–409. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Keller, R.M.: Formal Verification of Parallel Programs. Communications of the ACM 19, 371–384 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  9. Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathExplorer. Electr. Notes Theor. Comput. Sci. 55(2) (2001)

    Google Scholar 

  10. Havelund, K., Rosu, G.: Efficient monitoring of safety properties. STTT 6(2), 158–173 (2004)

    Article  Google Scholar 

  11. Katz, G., Peled, D.: Code Mutation in Verification and Automatic Code Generation. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 435–450. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. van der Meyden, R.: Common Knowledge and Update in Finite Environment. Information and Computation 140(2), 115–157 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  13. Orlin, J.: Contentment in Graph Theory: Covering Graphs with Cliques. Indagationes Mathematicae 80(5), 406–424 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  14. Pérez, J., Corchuelo, R., Toro, M.: An Order-based Algorithm for Implementing Multiparty Synchronization. Concurrency - Practice and Experience 16(12), 1173–1206 (2004)

    Article  Google Scholar 

  15. Thistle, J.G.: Undecidability in Decentralized Supervision. System and Control Letters 54, 503–509 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  16. Thomas, W.: On the Synthesis of Strategies in Infinite Games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  17. Tripakis, S.: Undecidable Problems of Decentralized Observation and Control on Regular Languages. Information Processing Letters 90(1), 21–28 (2004)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Graf, S., Peled, D., Quinton, S. (2011). Monitoring Distributed Systems Using Knowledge. 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_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-21461-5_12

  • 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)

Publish with us

Policies and ethics