Time Safety Analysis of Embedded Programs

Christoph Kirsch1, Marco Sanvido2, and Slobodan Matic
(Professor Thomas A. Henzinger)
(DARPA) SEC F33615-C-98-3614

We consider programs of the so-called embedded (E) machine, which is a virtual machine for coordinating the interaction between physical processes and software processes [1]. The E machine executes E code, the timing and control-flow part of a program that specifies the invocation of software processes relative to events. The software processes form the functional part of the program and among them we distinguish two kinds: drivers and tasks. All information between the environment and the tasks flows through drivers, software processes with negligible worst-case execution times (WCET). On the other hand, tasks model processes with nonnegligible WCETs. One way to generate E code is from Giotto, a language designed for multi-modal control applications, where each mode is specified with a set of tasks and drivers that are periodically invoked.

The project addresses the problem of checking whether all possible executions of a given E code program on a given platform satisfy certain timing requirements. The compiler that generates E code expects sufficient performance from the platform, so that the computation of a task always finishes before drivers update task inputs or read task outputs, and before another invocation of the task is scheduled. A trace that satisfies such implicit deadlines is called time safe because it meets all timing requirements of the E code.

In [2] we show that time-safety checking of arbitrary E code is computationally hard. However, a large class of real-time programs can be expressed as restricted subclasses of general E code. For example, a Giotto source program compiled into E code in a specific way can be checked in polynomial time. In this project we will try to exploit the E code structure further to construct efficient algorithms for time-safety checking. We envision an algorithm with two parts. It first computes the deadlines and then checks if the set of tasks with given WCETs and computed deadlines can be scheduled by a specified scheduling strategy. The algorithm does not interpret conditionals in the E code: the deadline is conservatively approximated as the minimum of the deadlines from the two branches of a conditional. The check is performed by building a program graph on E code extended with particular scheduler states.

T. A. Henzinger and C. M. Kirsch, "The Embedded Machine: Predictable, Portable Real-time Code," Proc. Conf. Programming Languages Design and Implementation, Berlin, Germany June 2002.
T. A. Henzinger, C. M. Kirsch, R. Majumdar, and S. Matic, "Time-Safety Checking for Embedded Programs," Proc. Int. Conf. Embedded Software, Grenoble, France, October 2002.
1Postdoctoral Researcher
2Postdoctoral Researcher

Send mail to the author : (matic@eecs.berkeley.edu)

Edit this abstract