Thursday Feb. 12, 2004, 4:15-5:45 pm, 3400 Boelter Hall

Embedded Software: Better Models, Better Code

Thomas A. Henzinger
University of California, Berkeley

Embedded software is increasingly deployed in safety-critical
applications, from medical implants to drive-by-wire technology.  This
calls for a rigorous design and verification methodology.  The main
difference between embedded and traditional software is that in the
embedded case non-functional aspects, such as reactivity with respect
to physical processes, resource usage, and timing, are integral to the
correct behavior of the software.  Yet traditional software
techniques, beginning with high-level programming languages, rarely
address these non-functional aspects; indeed, the systematic
abstraction of real time and other physical constraints has been one
of the great success stories in computer science, from Turing machines
to thread-based concurrency models.  For the principled design of
embedded software, instead, we have to recombine computation and
physicality.

We present one approach how such a recombination might be achieved.
We start with a programmer's model and the corresponding high-level
language which specifies both the functionality and the timing of an
embedded program.  It is now the job of the compiler to produce code
that implements the specified functionality and also the specified
timing.  In other words, the programmer specifies the reactivity of a
program, and the compiler checks its schedulability.  For this, the
compiler needs information about the platform, such as worst-case
execution times, but it produces deterministic code whose observable
behavior is independent of execution-time variations and scheduling
decisions.  Furthermore, the program can be recompiled on different
platforms and composed with other programs, without changing its
functionality nor its timing.  We have illustrated the effectiveness
of this approach by programming, once, the flight-control software of
several model helicopters with different hardware configurations.

Host: Jens Palsberg