Simulations between specifications of distributed systems | SpringerLink
Skip to main content
Springer Nature Link
Log in

Simulations between specifications of distributed systems

  • Selected Presentations
  • Conference paper
  • First Online:
CONCUR '91 (CONCUR 1991)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 527))

Included in the following conference series:

Abstract

In the stepwise development of a distributed system, the problem arises of verifying that a specification at a lower level of abstraction correctly implements a specification at a higher level of abstraction. Forward and backward simulation have been proposed as verification techniques for this problem. In this paper, we study forward and backward simulation in a framework where specifications are given as labeled transition systems with fairness requirements. We aim at clarifying the connection between simulations and the auxiliary variable constructions of Abadi and Lamport. In the paper, we also relax the earlier restriction that backward simulations be finitary. For a simple specification notation, similar to the action system formalism or Unity, we furthermore present proof rules that correspond to forward and backward simulations. Finally, we relate the forward and backward simulation techniques to subset-constructions that can be used in automata theory, e.g. for deciding language containment.

supported in part by the Swedish Board for Technical Development (STU) under contract No. 89-01220P as part of Esprit BRA project SPEC, No. 3096

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Abadi and L. Lamport. The existence of refinement mappings. In Proc. 3 rd IEEE Int. Symp. on Logic in Computer Science, Edinburgh, 1988.

    Google Scholar 

  2. R.J.R. Back and R. Kurki-Suonio. Distributed cooperation with action systems. ACM Trans. on Programming Languages and Systems, 10(4):513–554, Oct. 1988.

    Google Scholar 

  3. R.J.R. Back and K. Sere. Stepwise refinement of parallel algorithms. Technical Report A. 64, Åbo Akademi, Dept. of Computer Science and Mathematics, 1988.

    Google Scholar 

  4. K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

    Google Scholar 

  5. R. de Nicola and F.W. Vaandrager. Three logics for branching bisimulation. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science, pages 118–129, 1990.

    Google Scholar 

  6. R. Gerth. Foundations of compositional program refinement — safety properties. Volume 430 of Lecture Notes in Computer Science, pages 777–808. Springer Verlag, 1990.

    Google Scholar 

  7. C.A.R. Hoare, H. Jifeng, and J.W. Sanders. Prespecification in data refinement. Information Processing Letters, 25:71–76, 1987.

    Google Scholar 

  8. C.A.R. Hoare. Proof of correctness of data representation. Acta Informatica, 1(4):271–281, 1972.

    Google Scholar 

  9. J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

    Google Scholar 

  10. H. Jifeng. Process simulation and refinement. Formal Aspects of Computing, 1:229–241, 1989.

    Google Scholar 

  11. B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Dept. of Computer Systems, Uppsala University, Sweden, Uppsala, Sweden, 1987. Available as report DoCS 87/09.

    Google Scholar 

  12. B. Jonsson. Modular verification of asynchronous networks. In Proc. 6 th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 152–166, Vancouver, Canada, 1987. Extended Version as SICS Research Report R90010.

    Google Scholar 

  13. B. Jonsson. On decomposing and refining specifications of distributed systems. Volume 430 of Lecture Notes in Computer Science, pages 361–385. Springer Verlag, 1990.

    Google Scholar 

  14. M.B. Josephs. A state-based approach to communicating processes. Distributed Computing, 3:9–18, 1988.

    Google Scholar 

  15. A. Kleinman, Y. Moscowitz, A. Pnueli, and E. Shapiro. Communication with directed logic variables. In Proc. 18 th ACM Symp. on Principles of Programming Languages, 1991.

    Google Scholar 

  16. N. Klarlund and F.B. Schneider. Verifying safety properties using infinite-state automata. Technical Report TR 89-1039, Cornell University, Ithaca, New York, 1989.

    Google Scholar 

  17. L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systems, 5(2):190–222, 1983.

    Google Scholar 

  18. L. Lamport. A simple approach to specifying concurrent systems, Communications of the ACM, 32(1):32–45, Jan. 1989.

    Google Scholar 

  19. S.S. Lam and A.U. Shankar. Protocol verfication via projections. IEEE Trans. on Software Engineering, SE-10(4):325–342, July 1984.

    Google Scholar 

  20. S.S. Lam and A.U. Shankar. Refinement and projection of relational specifications. Volume 430 of Lecture Notes in Computer Science, pages 454–486. Springer Verlag, 1990.

    Google Scholar 

  21. N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6 th ACM Symp. on Principles of Distributed Computing, Vancouver, Canada, pages 137–151, 1987.

    Google Scholar 

  22. M. Merritt. Completeness theorems for automata. Volume 430 of Lecture Notes in Computer Science, pages 544–560. Springer Verlag, 1990.

    Google Scholar 

  23. R. Milner. An algebraic definition of simulation between programs. pages 481–489. Also as Report No. CS-205, Computer Science Department, Stanford University.

    Google Scholar 

  24. Z. Manna and A. Pnueli. The temporal framework for concurrent programs. In Boyer and Moore, editors, The Correctness Problem in Computer Science, pages 215–274. Academic Press, 1981.

    Google Scholar 

  25. Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4(4):257–289, 1984.

    Google Scholar 

  26. Z. Manna and A. Pnueli. The anchored version of the temporal framework. In de Bakker, de Roever, and Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 201–284. Springer Verlag, 1989.

    Google Scholar 

  27. T. Nipkow. Non-deterministic data types. Acta Informatica, 22:629–661, 1986.

    Google Scholar 

  28. F. Orava. Verifying safety and deadlock properties of networks of asynchronously communicating processes. In Proc. 9 th IFIP WG6.1 Symp. on Protocol Specification, Testing, and Verification, Twente, Holland, 1989.

    Google Scholar 

  29. G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark, 1981.

    Google Scholar 

  30. A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. Volume 224 of Lecture Notes in Computer Science, pages 510–584. Springer Verlag, 1986.

    Google Scholar 

  31. A.P. Sistla. On verifying that a concurrent program satisfies a non-deterministic specification. Technical Report TR 88-378.01.1, Computer and Intelligent Systems Lab. GTE Laboratories, May 1988.

    Google Scholar 

  32. A.U. Shankar and S.S. Lam. An HDLC protocol specification and its verification using image protocols. ACM Transactions on Computer Systems, 1(4):331–368, Nov. 1983.

    Google Scholar 

  33. E.W. Stark. Foundations of a Theory of Specification for Distributed Systems. PhD thesis, Massachussetts Inst. of Technology, 1984. Available as Report No. MIT/LCS/TR-342.

    Google Scholar 

  34. E.W. Stark. Proving entailment between conceptual state specifications. Theoretical Computer Science, 56:135–154, 1988.

    Google Scholar 

  35. M.Y. Vardi. Verification of concurrent programs: The automata theoretic framework. In Proc. 2 nd IEEE Int. Symp. on Logic in Computer Science, 1987.

    Google Scholar 

  36. J. Lundelius Welch, L. Lamport, and N. Lynch. A lattice-structured proof technique applied to a minimum spanning tree algorithm, July 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Swedish Institute of Computer Science, Stockholm

    Bengt Jonsson

  2. Dept. of Computer Systems, Uppsala University, Sweden

    Bengt Jonsson

  3. SICS, Box 1263, S-164 28, Kista, Sweden

    Bengt Jonsson

Authors
  1. Bengt Jonsson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jos C. M. Baeten Jan Frisco Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jonsson, B. (1991). Simulations between specifications of distributed systems. In: Baeten, J.C.M., Groote, J.F. (eds) CONCUR '91. CONCUR 1991. Lecture Notes in Computer Science, vol 527. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54430-5_99

Download citation

  • DOI: https://doi.org/10.1007/3-540-54430-5_99

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54430-2

  • Online ISBN: 978-3-540-38357-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation