We propose to develop a theory for the composition and analysis of ?rich API?s? for embedded systems, which expose resource properties, such as real-time assumptions and guarantees. We will apply this theory to both time-triggered programs,in particular to proposed real-time Linux standards and protocols under design at the Berkeley Wireless Research Center.

We propose to develop a theory of an open system of type qualifiers, which allow programmers to assert properties of program behavior in a simple extension of standard type systems. Types may be annotated with qualifiers expressing arbitrary program properties and these qualifiers will be automatically checked as part of an extended typechecking
procedure.

We will develop a number of applications for, and experimentally evaluate, a prototype type qualifier system. Inference algorithms will be developed to alleviate the need for programmers to extensively annotate programs. Applications will include examples from embedded systems to check critical system properties.We will also investigate using qualifiers as an aid to software model checking.