Environment-based Development of Reactive Systems

  • Yves Ledru
  • Pierre Collette
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


This paper presents an approach for the specification and design of reactive systems where the environment is the starting point of the development process. This environment subsequently provides a proving context for the design and validation activities. In this paper, the approach is used within Lamport’s TLA framework. A case study clearly shows the benefits of the method at the specification stage where it prevents overspecification. The paper then explores and discusses the design and validation of a program for the controller. The discussion tries to make more precise the nature of the elementary development steps and to point out specific steps in the development of reactive applications.


Reactive System Temporal Logic Design Decision Customer Orientation Mutual Exclusion 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. AL93] M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, january 1993.Google Scholar
  2. [BC85]
    G. Berry and I. Cosserat. The ESTEREL synchronous programming language and its mathematical semantics. In S. Brookes and G. Winskel, editors, Seminar on Concurrency, volume 197 of Lecture Notes in Computer Science, pages 389–449. Springer-Verlag, 1985.Google Scholar
  3. Bro89] M. Broy. Functional specification of communicating systems. In G.X. Ritter,editor, IFIP 89,pages 851–856.North-Holland,1989.Google Scholar
  4. [Bro90]
    M. Broy. On bounded buffers: Modularity, robustness, and reliability in reactive systems. In W. H. J. Feijen, A. J. M. Van gasteren, D. Gries, and J. Misra, editors, Beauty is our business - a birthday salute to Edsger W. Dijkstra, pages 83–93. Springer Verlag, 1990.Google Scholar
  5. [CL93]
    P. Collette and Y. Ledru: From environment to system specifications: Dining philosophers revisited. Technical report, Université Catholique de Louvain, Unité d’Informatique, 1993.Google Scholar
  6. [CM88]
    K. Chandy and J. Misra. Parallel Program Design: A Foundation.Addison-Wesley, 1988.Google Scholar
  7. [CPHP87]
    P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. LUSTRE: A declarative language for programming synchronous systems. In Proceedings of the 14th POPL, pages 178–188. ACM, 1987.Google Scholar
  8. [DAC+89]
    M. Diaz, J.-P. Ansart, J.-P. Courtiat, P. Azema, and V. Chari. The formal description technique Estelle - Results of the ESPRIT/SEDOS project. North Holland, 1989.Google Scholar
  9. [Ded90]
    F. Dederichs. System and environment: the philosophers revisited. Technical Report TUM-I9040, Technische Universität München, 1990.Google Scholar
  10. [DH87]
    E. Dubois and J. Hagelstein. Reasoning on formal requirements:a lift control system. In Proceedings of the fourth International Workshop on Software Specification and Design. IEEE Computer Society, 1987.Google Scholar
  11. [Dij71]
    E.W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica, 1 (2): 115–138, 1971.CrossRefMathSciNetGoogle Scholar
  12. [Dij78]
    E.W. Dijkstra. Two starvation free solutions to a general exclusion problem. Technical Report EWD 625, Plataanstraat 5, 5671 Al Nuenen, 1978.Google Scholar
  13. [Fea87]
    M.S. Feather. Language support for the specification and development of composite systems. ACM Transactions on Programming Languages and Systems,9(2):198–234, april 1987.Google Scholar
  14. [FM92]
    J. Fiadeiro and T. Maibaum. Temporal theories as modularization units for concurrent system specification. Formal Aspects of Computing, 4 (3): 239–272, 1992.CrossRefMATHGoogle Scholar
  15. [Har87]
    D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8 (3), 1987.Google Scholar
  16. [IS088]
    ISO. Lotos, a formal description technique based on the temporal ordering of observational behaviour. Technical Report ISO-DP-8807, International Organization for Standardisation, 1988.Google Scholar
  17. [Jac83]
    M.A. Jackson. System development. Prentice-Hall, 1983.Google Scholar
  18. [Jon90]
    C. B. Jones. Systematic Software Development Using VDM (Second Edition). Prentice-Hall, London, 1990.Google Scholar
  19. [Lam89]
    L. Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32 (1): 32–45, 1989.CrossRefMathSciNetGoogle Scholar
  20. [Lam91]
    L. Lamport. The temporal logic of actions. Technical Report SRC79, DEC Systems Research Center, Palo Alto, december 1991.Google Scholar
  21. [Led90]
    Y. Ledru. Hierarchical Specification of Reactive Systems: a case study. In Proceedings of the CompEuro’90 Conference, pages 109116. IEEE Computer Society Press, 1990.Google Scholar
  22. [Led91]
    Y. Ledru. Towards the formal development of terminating reactive systems. PhD thesis, Université Catholique de Louvain, Unité d’Informatique, 1991.Google Scholar
  23. [Led93]
    Y. Ledru. Developing reactive systems in a VDM framework. Science of Computer Programming, 20 (1–2): 51–71, 1993.CrossRefMATHGoogle Scholar
  24. [LT90]
    N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the ACM Symposium on Principles of Distributed Computing. ACM, 1990.Google Scholar
  25. [MP92]
    Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems. Springer-Verlag, 1992.Google Scholar
  26. [Mu185]
    Geoff Mullery. Acquisition - environment. In M. Paul and H.J.Siegert, editors, Distributed Systems - Methods and Tools for Specification - An Advanced Course, volume 190 of Lecture Notes in Computer Science. Springer-Verlag, 1985.Google Scholar
  27. [Pnu86]
    A. Pnueli. Specification and development of reactive systems. In H.-J. Kugler, editor, IFIP 86, pages 845–858. North-Holland, 1986.Google Scholar
  28. [Pnu92]
    A. Pnueli. System specification and refinement in temporal logic. In R. Shyamasundar, editor, Software technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science. Springer-Verlag, 1992.Google Scholar
  29. [RE87]
    G.-C. Roman and M.E. Ehlers. System specifications and physical relevance. In Proceedings of the fourth International Workshop on Software Specification and Design. IEEE Computer Society, 1987.Google Scholar

Copyright information

© British Computer Society 1994

Authors and Affiliations

  • Yves Ledru
    • 1
  • Pierre Collette
    • 2
    • 3
  1. 1.Service d’InformatiqueFaculté Polytechnique de MonsMonsBelgium
  2. 2.National Fund for Scientific ResearchUniversité Catholique de LouvainLouvain-la-NeuveBelgium
  3. 3.Unité d’InformatiqueLouvain-la-NeuveBelgium

Personalised recommendations