Formal Derivation of Strongly Correct Concurrent Programs
(1979) Acta Informatica — Vol. 12, n° 1, p. 1-31 (1979)
Files
No attached file found for this publication.
Details
- Authors
- Abstract
- A method is described for deriving concurrent programs which are consistent with the problem specifications and free from deadlock and from starvation. The programs considered are expressed by nondeterministic repetitive selections of pairs of synchronizing conditions and subsequent actions. An iterative, convergent calculus is developed for synthesizing the invariant and synchronizing conditions which guarantee strong correctness. These conditions are constructed as limits of recurrences associated with the specifications and the actions. An alternative method for deriving starvationfree programs by use of auxiliary variables is also given. The applicability of the techniques presented is discussed through various examples; their use for verification purposes is illustrated as well.
- Affiliations
Citations
van Lamsweerde, A., & Sintzoff, M. (1979). Formal Derivation of Strongly Correct Concurrent Programs. Acta Informatica, 12(1), 1-31. https://hdl.handle.net/2078.5/204966 (Original work published 1979)