Real-Time Constraints Through the ProCoS Layers - Correct System Design: Recent Insights and Advances - page 75

This approach is well illustrated by the work by Dierks on PLC-automata [2].
An extension to such a framework could integrate model checking with proof
strategies for standard forms in a development tool.
A remaining concern is the link to the code and to a run time system. Veri-
ed compilers and compilers that check scheduling information are not common;
programming language technology has been geared more towards the large mar-
ket for general programming than the niche of embedded systems. Perhaps the
problem will be solved by integrated development environments that translate
directly from state machines to binary code, avoiding all the complications of
general purpose programming languages.
ProCoS is now in the past, but it has left the challenge to develop an engineer-
ing practise for embedded systems; a practise that is based on mathematically
sound techniques and linking top level requirements to the computer system at
the bottom. This was the vision of the ProCoS `fathers: Dines Bjrner, Tony
Hoare and Hans Langmaack.

Acknowledgment. We thank Tony Hoare and Ernst-Rudiger Olderog for instruc-
tivecommentsonpreviousdraftsofthispaper.

References

1. M. S. Branicky. Analyzing and synthesizing hybrid control systems. In G. Rozen-
berg and F. W. Vaandrager, editors, Embedded Systems , volume 1494 of LNCS ,
pages 74{113. Springer-Verlag, 1998.
2. H. Dierks. PLC-Automata: A New Class of Implementable Real-Time Automata.
In M. Bertran and T. Rus, editors, Transformation-Based Reactive Systems Devel-
opment (ARTS'97) , volume 1231 of LNCS , pages 111{125. Springer-Verlag, 1997.
3. M. R. Hansen and Zhou Chaochen. Duration calculus: Logical foundations. Formal
Aspects of Computing , 9(3):283{33, 1997.
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.
5. H. Langmaack. The ProCoS approach to correct systems. Real-Time Systems ,

13:253{275, 1997.
6. H. Langmaack and A. P. Ravn. The ProCoS project: Provably correct systems. In
J. Bowen, editor, Towards Veried Systems , volume 2 of Real-Time Safety Critical
Systems , chapter Appendix B. Elsevier, 1994.
7. Z. Liu. Specication and verication in dc. In Mathai Joseph, editor, Mathematics
of Dependable Systems , Intnl. Series in Computer Science, chapter 7, pages 182{
228. Prentice Hall, 1996.
8. M. Muller-Olm. Modular Compiler Verication , volume 1283 of LNCS. Springer-

Verlag, 1997.
9. E-R. Olderog, A. P. Ravn, and J. U. Skakkebk. Rening system requirements to
program specications. In C. Heitmeyer and D. Mandrioli, editors, Formal Methods
in Real-Time Systems , Trends in Software-Engineering, chapter 5, pages 107{134.
Wiley, 1996.