Time-Safety Checking for Embedded Programs
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.
Unable to display preview. Download preview PDF.
- 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
- 3.N. Halbwachs. Synchronous Programming of Reactive Systems. Kluwer, 1993.Google Scholar
- 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