Real-Time Constraints Through the ProCoS Layers
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.
Keywordsembedded system hybrid system real-time, requirements design, formal specification
Unable to display preview. Download preview PDF.
- 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.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
- 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.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.M. Müller-Olm. Modular Compiler Verification, volume 1283 of LNCS. Springer-Verlag, 1997.Google Scholar
- 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.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
- 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.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.Chaochen Zhou, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Proc. Letters, 40(5), Dec. 1991.Google Scholar