Compilation and Synthesis for Real-Time Embedded Controllers

  • Martin Fränzle1
  • Markus Müller-Olm
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1710)


This article provides an overview over two constructive approaches to provably correct hard real-time code generation where hard real-time code is generated from abstract requirements rather than verified against the timing requirements a posteriori. The first, more pragmatic approach is concerned with translation of imperative programs, extended by hard real-time commands which allow one to specify upper bounds for the execution time of basic blocks. In the second approach, Duration Calculus, a metric-time temporal logic, is used as the source language. Duration Calculus allows one to specify real-time systems at a very high level of abstraction.


Control Problem Abstraction Level Regular Language Synthesis Problem Source Language 
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. 1.
    R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    E. Asarin, P. Caspi, and O. Maler. A Kleene theorem for timed automata. In G. Winskel, editor, 12th Annual IEEE Symposium on Logic in Computer Science (LICS‘97). IEEE Computer Society Press, 1997.Google Scholar
  3. 3.
    E. Asarin, O. Maler, and A. Pnueli. Symbolic controller synthesis for discrete and timed systems. In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, LNCS 999, Springer-Verlag, 1995.Google Scholar
  4. 4.
    R. J. R. Back and J. von Wright.Refinement calculus, Part I: Sequential nondeterministic programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Re nement of Distributed Systems-Models, Formalisms, Correctness. REX Workshop, LNCS 430, pages 42–66, Springer-Verlag, 1989.Google Scholar
  5. 5.
    R. J. R. Back and J. von Wright. Duality in specification languages: A lattice theoretic approach. Acta Informatica, 27(7):583–625, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language, and Interaction: Essays in Honour of Robin Milner. MITPress, to appear.Google Scholar
  7. 7.
    W. R. Bevier, W. A. Hunt, J S. Moore, and W. D. Young. Special issue on system verification. Journal of Automated Reasoning, 5(4), 1989.Google Scholar
  8. 8.
    J. P. Bowen, C. A. R. Hoare, H. Langmaack, E.-R. Olderog, and A. P. Ravn. A ProCoS II project final report: ESPRIT Basic Research project 7071. Bulletin of the European Association for Theoretical Computer Science (EATCS), 59, 1996.Google Scholar
  9. 9.
    J. P. Bowen, M. Fränzle, E.-R. Olderog, and A. P. Ravn. Developing correct systems. In Proc. 5th Euromicro Workshop on Real-Time Systems, Oulu, Finland, pages 176–189. IEEE Computer Society Press, 1993.Google Scholar
  10. 10.
    G. M. Brown. Towards truly delay-insensitive circuit realizations of process algebras. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, Workshops in Computing, pages 120–131. Springer-Verlag, 1991.Google Scholar
  11. 11.
    H. Dierks. Synthesizing controllers from real-time specifications. In Tenth International Symposium on System Synthesis (ISSS’ 97), pages 126–133. IEEE Computer Society Press, 1997.Google Scholar
  12. 12.
    E. W. Dijkstra.A Discipline of Programming. Prentice Hall, 1976.Google Scholar
  13. 13.
    M. Fränzle. Synthesizing controllers from duration calculus. In B. Jonsson and J. Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’ 96), LNCS 1135, pages 168–187, Springer-Verlag, 1996.Google Scholar
  14. 14.
    M. Fränzle. Controller Design from Temporal Logic:Undecidability need not matter. Dissertation, Technische Fakultät der Christian-Albrechts-Universität Kiel, Germany, 1997. Available as Bericht Nr. 9710, Institut für Informatik und Prakt. Mathematik der Christian-Albrechts-Universität Kiel, Germany, and via WWW under URL
  15. 15.
    M. Fränzle and M. Müller-Olm. Towards provably correct code generation for a hard real-time programming language. In P. A. Fritzson, editor, Compiler Construction ‘94, 5th International Conference Edinburgh U.K., LNCS 786, pages 294–308, Springer-Verlag, 1994.Google Scholar
  16. 16.
    P. H. B. Gardiner and C. C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87, 1991. Also in [32].Google Scholar
  17. 17.
    J. D. Guttman, J. D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5–32, 1995.Google Scholar
  18. 18.
    N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.Google Scholar
  19. 19.
    He Jifeng, I. Page, and J. P. Bowen. Towards a provably correct hardware implementation of Occam. In G. J. Milne and L. Pierre, editors, Correct Hardware Design and Veri cation Methods, LNCS 683, pages 214–225. Springer-Verlag, 1993.CrossRefGoogle Scholar
  20. 20.
    C. A. R. Hoare. Refinement algebra proves correctness of compiling specifications. In C. C. Morgan and J. C. P. Woodcock, editors, 3rd Re nement Workshop, Workshops in Computer Science, pages 33–48. Springer-Verlag, 1991.Google Scholar
  21. 21.
    C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A.W. Roscoe, J. W. Sanders, I. H. Sorenson, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672–687, 1987.zbMATHCrossRefGoogle Scholar
  22. 22.
    C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701–739, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    inmos limited. Transputer Instruction Set-A Compiler Writer’s Guide. Prentice Hall International, first edition, 1988.Google Scholar
  24. 24.
    J. J. Joyce. Totally verified systems: Linking verified software to verified hardware. In Leeser and Brown [25], pages 177–201.Google Scholar
  25. 25.
    M. Leeser and G. Brown, editors. Hardware Speci cation, Verification and Synthesis: Mathematical Aspects, LNCS 408, Springer-Verlag, 1990.Google Scholar
  26. 26.
    O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In Meyer and Puech [29], pages 229–242.Google Scholar
  27. 27.
    A. J. Martin. The design of a delay-insensitive microprocessor: An example of circuit synthesis by program transformation. In Leeser and Brown [25], pages 244–259.Google Scholar
  28. 28.
    J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In J. Schwarz, editor, Proc. Symp. Applied Mathematics, pages 33–41. American Mathematical Society, 1967.Google Scholar
  29. 29.
    E.W. Meyer and C. Puech, editors. Symposium on Theoretical Aspects of Computer Science (STACS 95), LNCS 900, Springer-Verlag, 1995.Google Scholar
  30. 30.
    R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.Google Scholar
  31. 31.
    J S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.Google Scholar
  32. 32.
    C. Morgan and T. Vickers (Eds.). On the Refinement Calculus. Springer-Verlag, 1994.Google Scholar
  33. 33.
    F. L. Morris. Advice on structuring compilers and proving them correct. In Proceedings ACM Symposium on Principles of Programming Languages (PoPL‘93), pages 144–152, 1973.Google Scholar
  34. 34.
    J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  35. 35.
    J. M. Morris. Laws of data refinement. Acta Informatica, 26:287–308, 1989.zbMATHMathSciNetGoogle Scholar
  36. 36.
    M. Müller-Olm. A short description of the prototype compiler. ProCoS Technical Report Kiel MMO 14/1, Christian-Albrechts-Universität Kiel, Germany, August 1995.Google Scholar
  37. 37.
    M. Müller-Olm. Modular Compiler Verification: A Process-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283, Springer-Verlag, 1997.Google Scholar
  38. 38.
    T. S. Norvell. Machine code programs are predicates too. In D. Till, editor, 6th Refinement Workshop, Workshops in Computing. Springer-Verlag and British Computer Society, 1994.Google Scholar
  39. 39.
    D. J. Pavey and L. A. Winsborrow. Demonstrating equivalence of source code and PROM contents. The Computer Journal, 36(7):654–667, 1993.CrossRefGoogle Scholar
  40. 40.
    A. P. Ravn. Design of Embedded Real-Time Computing Systems. Doctoral dissertation, Department of Computer Science, Danish Technical University, Lyngby, DK, 1995. Available as technical report ID-TR: 1995-170.Google Scholar
  41. 41.
    A. P. Ravn, H. Rischel, and K. M. Hansen. Specifying and verifying requirements of real-time systems. IEEE Transactions on Software Engineering, 19(1):41–55, 1993.CrossRefGoogle Scholar
  42. 42.
    A. P. Ravn and H. Rischel. Real-time constraints in the ProCoS layers. In E. R. Olderog and B. Steffen, editors, Correct System Design, this volume.Google Scholar
  43. 43.
    J. W. Thatcher, E. G. Wagner, and J. B. Wright. More on advice on structuring compilers and proving them correct. Theoretical Computer Science, 15:223–249, 1981.zbMATHCrossRefGoogle Scholar
  44. 44.
    W. Thomas. On the synthesis of strategies in infinite games. In Meyer and Puech [29], pages 1–13.Google Scholar
  45. 45.
    T. Wilke. Automaten und Logiken zur Beschreibung zeitabhängiger Systeme. Dissertation, Technische Fakultät der Christian-Albrechts-Universität Kiel, Germany, 1994.Google Scholar
  46. 46.
    T. Wilke. Specifying timed state sequences in powerful decidable logics and timed automata. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’ 94), LNCS 863, pages 694–715, Springer-Verlag, 1994.Google Scholar
  47. 47.
    M.W. Wilkes and J. B. Stringer. Micro-programming and the design of the control circuits in an electronic digital computer. Proc. Cambridge Phil. Soc., 49:230–238, 1953. also Annals of Hist. Comp. 8, 2 (dy1986) 121-126.zbMATHMathSciNetCrossRefGoogle Scholar
  48. 48.
    Zhou Chaochen, M. R. Hansen, and P. Sestoft. Decidability and undecidability results for duration calculus. In P. Enjalbert, A. Finkel, and K. W. Wagner, editors, Symposium on Theoretical Aspects of Computer Science (STACS 93), LNCS 665, pages 58–68, Springer-Verlag, 1993.Google Scholar
  49. 49.
    Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Martin Fränzle1
    • 1
  • Markus Müller-Olm
    • 2
  1. 1.Carl v. Ossietzky UniversitätDepartment of Computer ScienceGermany
  2. 2.University of DortmundDepartment of Computer ScienceGermany

Personalised recommendations