Abstract
We explain a transformational approach to the design and verification of communicating concurrent systems. The transformations start form specifications that combine trace-based with state-based assertional reasoning about the desired communication behaviour, and yield concurrent implementations. We illustrate our approach by a case study proving correctness of implementations of safe and regular registers allowing concurrent writing and reading phases, originally due to Lamport.
This research was partially supported by the CEC with the ESPRIT Basic Research Project No. 7071 ProCoS II and by the German Ministry of Research and Technologie (BMFT) as part of the project KORSO (Korrekle Software) under grant No. 01 IS 203 N.
Chapter PDF
Similar content being viewed by others
Keywords
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
R.J.R. Back. Refinement calculus, Part II: Parallel and Reactive Programs. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems — Models, Formalisms, Correctness, LNCS 430, pages 67–93. Springer-Verlag, 1990.
F.L. Bauer et al. The Munich Project CIP, Vol. II: The Transformation System CIP-S. LNCS 292. Springer-Verlag, 1987.
D. Bjørner et al. A ProCoS project description—ESPRIT BRA 3104. EATCS Bulletin, 39:60–73, 1989.
J.C.M. Baeten and P. Weijland. Process Algebra. Cambridge University Press, 1990.
R.H. Campbell and A.N. Habermann. The specification of process synchronisation by path expressions. LNCS 16. Springer-Verlag, 1974.
K.M. Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley, 1988.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, London, 1985.
B. Krieg-Brückner. Algebraic specification and functionals for transformational program and meta program development. In J. Diaz and F. Orejas, editors, Proc. TAP-SOFT '89, LNCS 352. Springer-Verlag, 1989.
L. Lamport. On interprocess communications II. Distributed Comp., 1:86–101, 1986.
N.A. Lynch and K.J. Goldman. Distributed algorithms. Technical Report MIT/LCS/RSS 5 6.852 Fall 1988, MIT, 1989.
N.A. Lynch and M.R. Tuttle. An introduction to input/ouput automata. Technical Report CWI-Quaterly 2(3), CWI, 1989.
R. Milner. Communication and Concurrency. Prentice Hall, London, 1989.
C. Morgan. Programming from Specifictions. Prentice Hall, London, 1990.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems — Specification. Springer-Verlag, 1991.
E.-R. Olderog. Nets, Terms and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press, 1991.
E.-R. Olderog. Towards a Design Calculus for Communicating Programs. In J.C.M. Baeten and J.F. Groote, editors, Proc. CONCUR '91, LNCS 527, pages 61–77. Springer-Verlag, 1991. invited paper.
E.-R. Olderog, S. Rössig, J. Sander, and M. Schenke. ProCoS at Oldenburg: The Interface between Specification Language and occam-like Programming Language. Technical Report Bericht 3/92, Univ. Oldenburg, Fachbereich Informatik, 1992.
S. Rössig and M. Schenke. Specification and stepwise development of communicating systems. In S. Prehn and W.J. Toetenel, editors, VDM'91 Formal Software Development Methods, LNCS 551, pages 149–163. Springer-Verlag, 1991.
J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, London, 1989.
A. Sprock. Spezifikation von Registern und Verifikation der Implementation von Registern. Studienarbeit, Univ. Oldenburg, 1992.
J. Zwiers. Compositionalty, Concurrency and Partial Correctness — Proof Theories for Networks of Processes and Their Relationship. LNCS 321. Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Olderog, ER., Rössig, S. (1993). A case study in transformational design of concurrent systems. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_58
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_58
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive