Abstract
This paper presents a transformational approach to the design of distributed systems where environment and concurrently running components communicate via synchronous message passing along directed channels. System specifications that combine trace-based with state-based reasoning are gradually modified by application of transformation rules until occam-like programs are achieved finally. We consider interactive and automatic aspects of such a design process and illustrate our approach by sketching the development of a shared register implementation.
This research was partially supported by the CRC with the ESPRIT Basic Research Project No. 7071 ProCoS II, by the German Ministry of Research and Technology (BMFT) as part of the project KORSO under grant No. 01 IS 203 N and by the Deutsche Forschungsgemeinschaft under grant No. 01 98/1-1.
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, Formalisrns, Correctness, LNCS 430, pages 67–93. Springer-Verlag, 1990.
J. Bohn and H. Hungar. Traverdi — Transformation and Verification of Distributed Systems. In M. Broy and S. Jänichen, editors, KORSO Correct Software by Formal Methods, LNCS. Springer-Verlag, 1995. to appear.
J. Bohn and S. Rössig. Towards a design assistant for communicating systems. ProCoS Doc. Id. OLD JB 2/1, Univ. Oldenburg — FB Informatik, 1995. URL: ftp://ftp.informatik.uni-oldenburg.de/pub/procos/JB-2-1.ps.z
K.M. Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley, 1988.
M. Francis, S. Finn, R.B. Hughes, and E. Mayger. LAMBDA Version 4.3, Documentation Set. Abstract Hardware Limited, London, 1993.
M. Fourman and E. Mayger. Integration of formal methods with system design. In Proc. VLSI'91, Edingburgh, 1991.
INMOS Ltd. occam 2 Reference Manual. Prentice Hall, 1988.
K.M. Jensen, H. Rischel, E.-R. Olderog, and S. Rössig. Syntax and informal semantics of the ProCoS specification language level 0. Technical Report ESPRIT Basic Research Action ProCoS, Doc. Id. ID/DTH KM.I 4/2, Technical University of Denmark, Lyngby, Dept. Comput. Sci., 1990.
L. Lamport. On interprocess communications Part II. Distributed Comp., 1:86–101, 1986.
L. Lamport. The temporal logic of actions. TOPLAS, 16(3):872–923, 1994.
N.A. Lynch and K.J. Goldman. Distributed algorithms. Technical Report MIT/LCS/RSS 5 6.852 Fall 1988, MIT, 1989.
E.-R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Inform., 23:9–66, 1986.
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.
E.-R. Olderog and S. Rössig. A case study in transformational design of concurrent systems. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT'93: Theory and Practice of Software Development, LNCS 668, pages 90–104. Springer-Verlag, 1993.
S. Rössig. A Transformational Approach to the Design of Communicating Systems. PhD thesis, Tech. report 4-94, Univ. Oldenburg — FB Informatik, 1994. URL: ftp://ftp.informatik.uni-oldenburg.de/pub/procos/PhD-roessig.ps.gz
J.M. Spivey. The Z Notation: A Reference Manual Prentice Hall, London, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bohn, J., Rössig, S. (1995). On automatic and interactive design of communicating systems. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1995. Lecture Notes in Computer Science, vol 1019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60630-0_11
Download citation
DOI: https://doi.org/10.1007/3-540-60630-0_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60630-7
Online ISBN: 978-3-540-48509-4
eBook Packages: Springer Book Archive