Advertisement

Development of concurrent systems by incremental transformation

  • E. Pascal Gribomont
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 432)

Abstract

A formal development method for concurrent programs is proposed. It generalizes several variants of the stepwise refinement method often used in concurrency, in that not only atomicity refinements, but also arbitrary transformations, are taken into account. The method is illustrated by simple examples.

Keywords

Deduction System Mutual Exclusion Concurrent Program Concurrent System Liveness Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [1]
    E.A. ASHCROFT and Z. MANNA, “Formalization of Properties of Parallel Programs”, Machine Intelligence, 6, pp. 17–41, 1970Google Scholar
  2. [2]
    K.R. APT, “Ten years of Hoare logic”, ACM Toplas, 3, pp. 431–483, 1981CrossRefGoogle Scholar
  3. [3]
    K.R. APT, “Correctness Proofs of Distributed Termination Algorithms”, ACM Toplas, 8, pp. 388–405, 1986CrossRefGoogle Scholar
  4. [4]
    R.J.R. BACK and R. KURKI-SUONIO, “Decentralization of Process Nets with Centralized Control”, Proc. 2nd ACM Symp. on Principles of Distributed Computing, pp. 131–142, 1983Google Scholar
  5. [5]
    R.J.R. BACK and R. KURKI-SUONIO, “Distributed Cooperation with Action Systems”, ACM Toplas, 10, pp. 513–554, 1988CrossRefGoogle Scholar
  6. [6]
    R.J.R. BACK, “A Calculus of Refinements for Program Derivations”, Acta Informatica, 25, pp. 593–624, 1988CrossRefGoogle Scholar
  7. [7]
    R.J.R. BACK, “A Method for Refining Atomicity in Parallel Algorithms”, LNCS, 366, pp. 199–216, 1989Google Scholar
  8. [8]
    E. BEST, “A Note on the Proof of a Concurrent Program”, IPL, 9, pp. 103–104, 1979Google Scholar
  9. [9]
    M. CHANDY and J. MISRA, “An Example of Stepwise Refinement of Distributed Programs: Quiescence Detection”, ACM Toplas, 8, pp. 326–343, 1986CrossRefGoogle Scholar
  10. [10]
    M. CHANDY and J. MISRA, “Parallel Program Design: A Foundation”, Addison-Wesley, 1988Google Scholar
  11. [11]
    J. de BAKKER, “Mathematical theory of program correctness”, Prentice-Hall, 1980Google Scholar
  12. [12]
    J.W. de BAKKER and L.G.L.T. MEERTENS, “On the completeness of the inductive assertion method”, JCSS, 11, pp. 323–357, 1975Google Scholar
  13. [13]
    E.W. DIJKSTRA, “A discipline of programming”, Prentice Hall, New Jersey, 1976Google Scholar
  14. [14]
    E.W. DIJKSTRA and al., “On-the-Fly Garbage Collection: An Exercise in Cooperation”, CACM, 21, pp. 966–975, 1978Google Scholar
  15. [15]
    E.W. DIJKSTRA, “An assertional proof of a program by G.L. Peterson”, EWD 779, 1981Google Scholar
  16. [16]
    R. GERTH, “Transition logic”, Proc. 16th ACM Symp. on Theory of Computing, pp. 39–50, 1984Google Scholar
  17. [17]
    E.P. GRIBOMONT, “Synthesis of parallel programs invariants”, LNCS, 186, pp. 325–338, 1985Google Scholar
  18. [18]
    E.P. GRIBOMONT, “Development of concurrent programs: an example” LNCS, 352, pp. 210–224, 1989Google Scholar
  19. [19]
    E.P. GRIBOMONT, “Stepwise refinement and concurrency: a small exercise” LNCS, 375, pp. 219–238, 1989Google Scholar
  20. [20]
    E.P. GRIBOMONT, “Stenning's protocol”, in “Formal methods for parallel programming”, Internal report, 1989Google Scholar
  21. [21]
    D. GRIES, “The Science of Programming”, Springer-Verlag, Berlin, 1981Google Scholar
  22. [22]
    C.A.R. HOARE, “An axiomatic basis for computer programming”, CACM, 12, pp. 576–583, 1969Google Scholar
  23. [23]
    C.A.R. HOARE, “Communicating Sequential Processes”, CACM, 21, pp. 666–677, 1978Google Scholar
  24. [24]
    C.A.R. HOARE, “Communicating Sequential Processes”, Prentice-Hall, 1985Google Scholar
  25. [25]
    R.M. KELLER, “Formal Verification of Parallel Programs”, CACM, 19, pp. 371–384, 1976Google Scholar
  26. [26]
    L. LAMPORT, “The ‘Hoare Logic’ of Concurrent Programs”, Acta Informatica, 14, pp. 21–37, 1980CrossRefGoogle Scholar
  27. [27]
    L. LAMPORT, “An Assertional Correctness Proof of a Distributed Algorithm”, SCP, 2, pp. 175–206, 1983Google Scholar
  28. [28]
    L. LAMPORT and F.B. SCHNEIDER, “The ‘Hoare Logic’ of CSP, and All That”, ACM Toplas, 6, pp. 281–296, 1984CrossRefGoogle Scholar
  29. [29]
    L. LAMPORT, “win and sin: Predicate Transformers for Concurrency”, DEC SRC Report 17, 1987Google Scholar
  30. [30]
    L. LAMPORT, “A Theorem on Atomicity in Distributed Algorithms”, DEC SRC Report 28, 1988Google Scholar
  31. [31]
    R.J. LIPTON, “Reduction: a method of proving properties of parallel programs”, CACM, 18, pp. 717–721, 1975Google Scholar
  32. [32]
    N.A. LYNCH and M.R. TUTTLE, “Hierarchical Correctness Proofs for Distributed Algorithms”, Proc. 6th ACM Symp. on Principles of Distributed Computing, pp. 137–151, 1987Google Scholar
  33. [33]
    Z. MANNA and A. PNUELI, “How to cook a temporal proof system for your pet language”, Proc. 10th ACM Symp. on Principles of Programming Languages, pp. 141–154, 1983Google Scholar
  34. [34]
    Z. MANNA and A. PNUELI, “Adequate proof principles for invariance and liveness properties of concurrent programs”, SCP, 4, pp. 257–289, 1984Google Scholar
  35. [35]
    Z. MANNA and A. PNUELI, “Specification and verification of concurrent programs by ∨-automata, Proc. 14th ACM Symp. on Principles of Programming Languages, pp. 1–12, 1987Google Scholar
  36. [36]
    C. MORGAN, “The Specification Statement”, ACM Toplas, 10, pp. 403–419, 1988CrossRefGoogle Scholar
  37. [37]
    J.M. MORRIS, “A theoretical basis for stepwise refinement and the programming calculus”, SCP, 9, pp. 287–306, 1987Google Scholar
  38. [38]
    S. OWICKI and D. GRIES, “An Axiomatic Proof Technique for Parallel Programs”, Acta Informatica, 6, pp. 319–340, 1976CrossRefGoogle Scholar
  39. [39]
    G.L. PETERSON, “Myths about the mutual exclusion problem”, IPL, 12, pp. 115–116, 1981Google Scholar
  40. [40]
    R.D. SCHLICHTING and F.D. SCHNEIDER, “Using Message Passing for Distributed Programming: Proof Rules and Disciplines”, ACM Toplas, 6, pp. 402–431, 1984CrossRefGoogle Scholar
  41. [41]
    J. SIFAKIS, “A unified approach for studying the properties of transition systems”, TCS, 18, pp. 227–259, 1982CrossRefGoogle Scholar
  42. [42]
    N.V. STENNING, “A data transfer protocol”, Computer Networks, 1, pp. 99–110, 1976CrossRefGoogle Scholar
  43. [43]
    A. van LAMSWEERDE and M. SINTZOFF, “Formal derivation of strongly correct concurrent programs”, Acta Informatica, 12, pp. 1–31, 1979Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • E. Pascal Gribomont
    • 1
  1. 1.Philips Research LaboratoryBrusselsBelgium

Personalised recommendations