Advertisement

Time-Safety Checking for Embedded Programs

  • Thomas A. Henzinger
  • Christoph M. Kirsch
  • Rupak Majumdar
  • Slobodan Matic
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2491)

Abstract

Giotto is a platform-independent language for specifying software for high-performance control applications. In this paper we present a new approach to the compilation of Giotto. Following this approach, the Giotto compiler generates code for a virtual machine, called the E machine, which can be ported to different platforms. The Giotto compiler also checks if the generated E code is time safe for a given platform, that is, if the platform offers sufficient performance to ensure that the E code is executed in a timely fashion that conforms with the Giotto semantics. Time-safety checking requires a schedulability analysis. We show that while for arbitrary E code, the analysis is exponential, for E code generated from typical Giotto programs, the analysis is polynomial. This supports our claim that Giotto identifies a useful fragment of embedded programs.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    K. Altisen, G. Gössler, A. Pnueli, J. Sifakis, S. Tripakis, and S. Yovine. A framework for scheduler synthesis. In Proc. Real-Time Systems Symp., pp. 154–163. IEEE Computer Society, 1999.Google Scholar
  2. 2.
    J.R. Büchi and L.H. Landweber. Solving sequential conditions by finite-state strategies. Trans. AMS, 138:295–311, 1969.CrossRefGoogle Scholar
  3. 3.
    N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.Google Scholar
  4. 4.
    T.A. Henzinger, B. Horowitz, and C.M. Kirsch. Giotto: a time-triggered language for embedded programming. In Proc. Embedded Software, LNCS 2211, pp. 166–184. Springer, 2001.CrossRefGoogle Scholar
  5. 5.
    T.A. Henzinger and C.M. Kirsch. The embedded machine: predictable, portable real-time code. In Proc. Conf. Programming Languages Design and Implementation, pp. 315–326. ACM, 2002.Google Scholar
  6. 6.
    C. Liu and J. Layland. Scheduling algorithms for multiprogramming in a hard-realtime environment. J. A CM, 20:46–61, 1973.zbMATHMathSciNetGoogle Scholar
  7. 7.
    J.W. Thatcher and J.B. Wright. Generalized finite-automata theory with an application to a decision problem in second-order logic. Mathematical Systems Theory, 2:57–81, 1968.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Thomas A. Henzinger
    • 1
  • Christoph M. Kirsch
    • 1
  • Rupak Majumdar
    • 1
  • Slobodan Matic
    • 1
  1. 1.Department of Electrical Engineering and Computer SciencesUniversity of CaliforniaBerkeleyUSA

Personalised recommendations