Specification and transformation of reactive systems with time restrictions and concurrency

  • Michael Schenke
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 863)


In this paper the most difficult step of a method is presented by which requirements in the duration calculus (DC) can be transformed into occam programs such that the implementation is correct by construction. Several rules for correct transformations from DC towards an important intermediate stage, the specification language SLtime, will be shown. In particular we shall explain the interplay between requirements and a control program, the introduction of parallelism and the change from the state based DC-description to the event based SLtimedescription.


correct software transformational design refinement real time concurrency 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BB90]
    J.C.M.Baeten, J.A.Bergstra. Real time process algebra. Formal Aspects of Computing 3(2), 1991, 142–188.Google Scholar
  2. [CHR92]
    Zhou Chaochen, C.A.R.Hoare, A.P.Ravn. A Calculus of Durations. IPL 40(5), 1992, 269–276.Google Scholar
  3. [Fr93]
    M.FrÄnzle. Proposal for a Programming Language Core for ProCoS II. ProCoS Project Document [MF 11/2], UniversitÄt Kiel.Google Scholar
  4. [HOS93]
    M.R.Hansen, E.-R. Olderog, M. Schenke. et al. A Duration Calculus Semantics for Real-Time Reactive Systems. ProCoS Project Document [OLD MRH 1/1], UniversitÄt Oldenburg, 1993.Google Scholar
  5. [Hoo91]
    J.J.M.Hooman. Specification and Compositional Verification of Real-Time Systems. LNCS 558 (Springer-Verlag, 1991).Google Scholar
  6. [MRR93]
    P.C.Masiero, A.P.Ravn, H.Rischel. Refinement of Real Time Specifications. ProCoS Project Document [ID/DTH PCM/0.1], Lyngby.Google Scholar
  7. [Mor90]
    C.Morgan. Programming from Specifications. Prentice Hall, 1990.Google Scholar
  8. [NSY91]
    X.Nicollin, J.Sifakis, S.Yovine. From ATP to Timed Graphs and Hybrid Systems. REX 1991, LNCS 600 (Springer-Verlag, 1991), 549–572.Google Scholar
  9. [Old92]
    E.-R.Olderog. Interfaces between Languages for Communicating Systems. ICALP 1992, LNCS 623 (Springer-Verlag, 1992), 641–655, invited paper.Google Scholar
  10. [ORSS92]
    E.-R.Olderog,S. Rössig, J.Sander, M. Schenke. ProCoS at Oldenburg: The Interface between Specification Language and occam-like Programming Language. Technical Report Bericht 3/92, Univ. Oldenburg 1992.Google Scholar
  11. [RRH93]
    A.P.Ravn, H.Rischel, K.M.Hansen. Specifying and Verifying Requirements of Real-Time Systems. IEEE Transactions on Software Engineering, vol. 19, 1 (1993) 41–55.Google Scholar
  12. [Sch93a]
    M.Schenke. A Timed Specification Language for Concurrent Reactive Systems. Workshop on the Semantics of Specification Languages, Utrecht 1993, Springer-Verlag, Workshops in Computing.Google Scholar
  13. [Sch93b]
    M.Schenke. Specification and Transformation of a Gas Burner. ProCoS Project Document [OLD MS 8/1], UniversitÄt Oldenburg, 1993.Google Scholar
  14. [SZH94]
    D.Scholefield, H.Zehan, He Jifeng. A Specification Oriented Semantics for the Refinement of Real-Time Systems, to appear in Theoretical Computer Science 1994.Google Scholar
  15. [Spi89]
    J.M.Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1989.Google Scholar
  16. [Zij88]
    E.Zijlstra. The railroad crossing. Deliverable, Esprit project DESCARTES, Foxboro, The Netherlands, 1988.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Michael Schenke
    • 1
  1. 1.Fachbereich InformatikUniversitÄt OldenburgOldenburgGermany

Personalised recommendations