Abstract
Designing parallel systems in a correct way is difficult. Transformational design of systems guarantees correctness by the correctness of the transformations, but is often tedious and complicated. We discuss different transformation strategies to guide the designer from the initial specification to different implementations, tailored to different architectures. Strategies give rise to simpler transformation rules, point the way in the design trajectory, and allow for the reuse of proofs and transformation steps when deriving optimizations and variants of algorithms.
This work was partially supported by the Deutsche Forschungsgemeinschaft under grant No. Ol 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. Back. Refinement calculus, Part II: Parallel and Reactive Programs. In de Bakker, de Roever, and Rozenberg, editors, Stepwise Refinement of Distributed Systems, LNCS 430, pages 67–93. Springer-Verlag, 1990.
R. Back and K. Sere. Stepwise refinement of action systems. Structured Programming 12:17–30, 1991.
P. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.
J. Bohn and W. Janssen. From a single specification to many implementations — many roads lead to parallelism. Technical report, University of Oldenburg, 1995. Available at ftp://ftp.Informatik.uni-oldenburg.de/pub/procos/.
J. Bohn and S. Rössig. On automatic and interactive design of communicating systems. In E. Brinksma, W. Cleaveland, K.G. Larsen, T. Margaria, and B. Steffen, editors, Proceedings of the First TACAS workshop, LNCS 1019, pages 216–247. Springer-Verlag, 1995.
R. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.
C. Chou and E. Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In Proceeding 7th ACM Symposium on Principles of Distributed Computing, 1988.
T. Elrad and N. Francez. Decomposition of distributed programs into communication closed layers. Science of Computer Programming, 2:155–173, 1982.
J. P. Bowen et al. A ProCoS II project description: ESPRIT Basic Research project 7071. Bulletin of the EATCS, 50:128–137, 1993.
C. Fischer. Transformation von synchronen SL-Specifikationen von Telekommunikationssytemen in asynchrone SL-Specifikationen. Master's thesis, University of Oldenburg, 1995. In German.
R. Gerth, R. Kuiper, and J. Segers. Interface refinement in reactive systems. In Proceedings CONCUR '92, LNCS 630, pages 77–94. Springer-Verlag, 1992.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
W. Janssen. Layered Design of Parallel Systems. PhD thesis, University of Twente, 1994.
W. Janssen, M. Poel, and J. Zwiers. Action systems and action refinement in the development of parallel systems. In Proceedings of CONCUR '91, LNCS 527, pages 298–316. Springer-Verlag, 1991.
L. Lamport. The Temporal Logic of Actions. ACMTOPLAS, 16(3):872–923, 1994.
C. Lengauer. Loop parallelization in the polytope model (invited talk). In Eike Best, editor, Proceedings CONCUR '93, LNCS 715, pages 398–416. Springer-Verlag, 1993.
E.-R. Olderog. Towards a design calculus for communicating programs (invited paper). In Proceedings of 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, LNCS 668, pages 90–104. Springer-Verlag, 1993.
E.-R. Olderog, S. Rössig, J. Sander, and M. Schenke. ProCoS at Oldenburg: The interface between specification language and occam-like programming language. Berichte aus dem Fachbereich Informatik 3, University of Oldenburg, 1992.
S. Rössig. A Transformational Approach to the Design of Communicating Systems. PhD thesis, University of Oldenburg, 1994.
J. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1989.
B. Steffen, T. Margaria, and A. Claßen. Heterogeneous analysis and verification for distributed systems. Technical Report MIP-9509, University of Passau, 1995.
F. Stomp. A derivation of a broadcasting protocol using sequentially phased reasoning (extended abstract). In L. Logrippo, R. Probert, and H. Ural, editors, Proceedings 10th IFIP symp. on Protocol Specification, Testing and Verification, pages 19–32. Elsevier Science Publishers, 1990.
F. Stomp and M. Siegel. Extending the limits of sequentially phased reasoning. In P. Thiagarajan, editor, Proceedings FST & TCS 14, LNCS 880. Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bohn, J., Janssen, W. (1996). A strategic approach to transformational design. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_110
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_110
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive