Advertisement

On automatic and interactive design of communicating systems

  • Jürgen Bohn
  • Stephan Rössig
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)

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.

Keywords

Regular Expression Transformation Rule Interactive Design Proof Obligation Trace Part 
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

  1. [Bac90]
    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.Google Scholar
  2. [BH94]
    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.Google Scholar
  3. [BR95]
    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.zGoogle Scholar
  4. [CM88]
    K.M. Chandy and J. Misra. Parallel Program Design — A Foundation. Addison-Wesley, 1988.Google Scholar
  5. [FFHM93]
    M. Francis, S. Finn, R.B. Hughes, and E. Mayger. LAMBDA Version 4.3, Documentation Set. Abstract Hardware Limited, London, 1993.Google Scholar
  6. [FM91]
    M. Fourman and E. Mayger. Integration of formal methods with system design. In Proc. VLSI'91, Edingburgh, 1991.Google Scholar
  7. [INM88]
    INMOS Ltd. occam 2 Reference Manual. Prentice Hall, 1988.Google Scholar
  8. [JROR90]
    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.Google Scholar
  9. [Lam86]
    L. Lamport. On interprocess communications Part II. Distributed Comp., 1:86–101, 1986.Google Scholar
  10. [Lam94]
    L. Lamport. The temporal logic of actions. TOPLAS, 16(3):872–923, 1994.Google Scholar
  11. [LG89]
    N.A. Lynch and K.J. Goldman. Distributed algorithms. Technical Report MIT/LCS/RSS 5 6.852 Fall 1988, MIT, 1989.Google Scholar
  12. [OH86]
    E.-R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Inform., 23:9–66, 1986.Google Scholar
  13. [Old91]
    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.Google Scholar
  14. [OR93]
    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.Google Scholar
  15. [Rös94]
    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.gzGoogle Scholar
  16. [Spi89]
    J.M. Spivey. The Z Notation: A Reference Manual Prentice Hall, London, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Jürgen Bohn
    • 1
  • Stephan Rössig
    • 1
  1. 1.FB InformatikC.V.O. Universität OldenburgOldenburgGermany

Personalised recommendations