# Development of concurrent systems by incremental transformation

Conference paper

First Online:

- 3 Citations
- 269 Downloads

## 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.

Download
to read the full conference paper text

## References

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