Real-Time Constraints Through the ProCoS Layers

  • Anders P. Ravn
  • Hans Rischel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)


The Provably Correct Systems project [5,6] developed links between layers of formal specifications for real-time systems. These layers cover requirements capture, design, programming and code generation. In this paper we trace real-time constraints through the layers in order to inspect their changing forms. They originate in constraints on continuous dynamical models of physical phenomena. However, in a digital system it is desirable to abstract the complexities of these models to simple clocks, and further to events in a reactive system. This paradigm is the main topic of this paper. We illustrate the different forms of timing constraints in duration calculus, a real-time interval logic.


embedded system hybrid system real-time, requirements design, formal specification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. S. Branicky. Analyzing and synthesizing hybrid control systems. In G. Rozenberg and F. W. Vaandrager, editors, Embedded Systems, volume 1494 of LNCS, pages 74–113. Springer-Verlag, 1998.Google Scholar
  2. 2.
    H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata. In M. Bertran and T. Rus, editors, Transformation-Based Reactive Systems Development (ARTS‘97), volume 1231 of LNCS, pages 111–125. Springer-Verlag, 1997.Google Scholar
  3. 3.
    M. R. Hansen and Zhou Chaochen. Duration calculus: Logical foundations. Formal Aspects of Computing, 9(3):283–33, 1997.zbMATHCrossRefGoogle Scholar
  4. 4.
    T. A. Henzinger, Z. Manna, and A. Pnueli. Timed transition systems. In J. W. de Bakker, C. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real-Time: Theory in Practice, REX Workshop, volume 600 of LNCS, pages 226–252. Springer-Verlag, 1992.CrossRefGoogle Scholar
  5. 5.
    H. Langmaack. The ProCoS approach to correct systems. Real-Time Systems, 13:253–275, 1997.CrossRefGoogle Scholar
  6. 6.
    H. Langmaack and A. P. Ravn. The ProCoS project: Provably correct systems. In J. Bowen, editor, Towards Verified Systems, volume 2 of Real-Time Safety Critical Systems, chapter Appendix B. Elsevier, 1994.Google Scholar
  7. 7.
    Z. Liu. Specification and verification in dc. In Mathai Joseph, editor, Mathematics of Dependable Systems, Intnl. Series in Computer Science, chapter 7, pages 182–228. Prentice Hall, 1996.Google Scholar
  8. 8.
    M. Müller-Olm. Modular Compiler Verification, volume 1283 of LNCS. Springer-Verlag, 1997.Google Scholar
  9. 9.
    E-R. Olderog, A. P. Ravn, and J. U. Skakkebæk. Refining system requirements to program specifications. In C. Heitmeyer and D. Mandrioli, editors, Formal Methods in Real-Time Systems, Trends in Software-Engineering, chapter 5, pages 107–134. Wiley, 1996.Google Scholar
  10. 10.
    A. P. Ravn, T. J. Eriksen, M. Holdgaard, and H. Rischel. Engineering of realtime systems with an experiment in hybrid control. In G. Rozenberg and F. W. Vaandrager, editors, Embedded Systems, volume 1494 of LNCS, pages 316–352. Springer-Verlag, 1998.Google Scholar
  11. 11.
    A.P. Ravn, H. Rischel, and K. M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng., 19(1):41–55, 1993.CrossRefGoogle Scholar
  12. 12.
    H. Rischel, J. Cuellar, S. Mørk, A. P. Ravn, and I. Wildgruber. Development of safety-critical real-time systems. In M. Bartošek, J. Staudek, and J. Wiedermann, editors, SOFSEM‘95: Theory and Practice of Informatics, volume 1012 of LNCS, pages 206–235. Springer-Verlag, 1995.Google Scholar
  13. 13.
    M. Schenke and A. P. Ravn. Refinement from a control problem to programs. In J. R. Abrial, E. Börger, and H. Langmaack, editors, Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, volume 1165 of LNCS, pages 403–427. Springer-Verlag, 1996.Google Scholar
  14. 14.
    Chaochen Zhou, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Proc. Letters, 40(5), Dec. 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Anders P. Ravn
    • 1
  • Hans Rischel
    • 2
  1. 1.Department of Computer ScienceAalborg UniversityDenmark
  2. 2.Department of Information TechnologyTechnical University of DenmarkDenmark

Personalised recommendations