Skip to main content
SpringerLink
Log in

Compilation and Synthesis for Real-Time Embedded Controllers

  • Chapter
  • First Online:
Correct System Design

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1710))

  • 356 Accesses

Abstract

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.

Acknowledgements

The research reported in this article has mainly been performed while the authors were with the Computer Science Department of the Christian-Albrechts-Universität Kiel, Germany, working in the ProCoS project and related projects under the supervision of Hans Langmaack. Over many years he strongly influenced the direction of our research through constant encouragement, insistence, and support. It is a great pleasure to present a summary of the results in a volume dedicated to him on the occasion of his retirement.

We thank the members of the ProCoS project for many fruitful discussions as well as J Moore and Bernhard Steffen for many valuable comments on a draft version of this article.We acknowledge the support of the European Union under grants ESPRIT BRA 3104 and 7071 and of the German Research Council DFG under contract DFG La 426/13-1,2.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. 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. R. J. R. Back and J. von Wright. Duality in specification languages: A lattice theoretic approach. Acta Informatica, 27(7):583–625, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. 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. 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. 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. 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. E. W. Dijkstra.A Discipline of Programming. Prentice Hall, 1976.

    Google Scholar 

  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. 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 http://ca.informatik.uni-oldenburg.de/~fraenzle/diss.html.

  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. P. H. B. Gardiner and C. C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87, 1991. Also in [32].

    Google Scholar 

  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. N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.

    Google Scholar 

  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.

    Chapter  Google Scholar 

  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. 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.

    Article  MATH  Google Scholar 

  22. C. A. R. Hoare, He Jifeng, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701–739, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  23. inmos limited. Transputer Instruction Set-A Compiler Writer’s Guide. Prentice Hall International, first edition, 1988.

    Google Scholar 

  24. J. J. Joyce. Totally verified systems: Linking verified software to verified hardware. In Leeser and Brown [25], pages 177–201.

    Google Scholar 

  25. M. Leeser and G. Brown, editors. Hardware Speci cation, Verification and Synthesis: Mathematical Aspects, LNCS 408, Springer-Verlag, 1990.

    Google Scholar 

  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. 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. 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. E.W. Meyer and C. Puech, editors. Symposium on Theoretical Aspects of Computer Science (STACS 95), LNCS 900, Springer-Verlag, 1995.

    Google Scholar 

  30. R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.

    Google Scholar 

  31. J S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996.

    Google Scholar 

  32. C. Morgan and T. Vickers (Eds.). On the Refinement Calculus. Springer-Verlag, 1994.

    Google Scholar 

  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. J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287–306, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  35. J. M. Morris. Laws of data refinement. Acta Informatica, 26:287–308, 1989.

    MATH  MathSciNet  Google Scholar 

  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. M. Müller-Olm. Modular Compiler Verification: A Process-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283, Springer-Verlag, 1997.

    Google Scholar 

  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. D. J. Pavey and L. A. Winsborrow. Demonstrating equivalence of source code and PROM contents. The Computer Journal, 36(7):654–667, 1993.

    Article  Google Scholar 

  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. 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.

    Article  Google Scholar 

  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. 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.

    Article  MATH  Google Scholar 

  44. W. Thomas. On the synthesis of strategies in infinite games. In Meyer and Puech [29], pages 1–13.

    Google Scholar 

  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. 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. 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.

    Article  MATH  MathSciNet  Google Scholar 

  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. Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carl v. Ossietzky Universität, Department of Computer Science, 26111, Oldenburg, Germany

    Martin Fränzle1

  2. University of Dortmund, Department of Computer Science, FB 4, LS 5, 44221, Dortmund, Germany

    Markus Müller-Olm

Authors
  1. Martin Fränzle1
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Markus Müller-Olm
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Fachbereich Informatik, Universität Oldenburg, Postfach 2503, D-26111, Oldenburg, Germany

    Ernst-Rüdiger Olderog

  2. Fachbereich Informatik, Universität Dortmund, Baroper Str. 301, D-44221, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Fränzle1, M., Müller-Olm, M. (1999). Compilation and Synthesis for Real-Time Embedded Controllers. In: Olderog, ER., Steffen, B. (eds) Correct System Design. Lecture Notes in Computer Science, vol 1710. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48092-7_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-48092-7_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66624-0

  • Online ISBN: 978-3-540-48092-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation