This project is concerned with models, techniques, and tools for specifying, analyzing, and generating software for real-time applications. Currently the emphasis is on requirements and design specifications, real-time operating systems, and methods for describing, predicting, and verifying the timing behavior of programming languages and systems. The research includes: using execution time bounds and assertional logic to state and prove timing properties of higher-level language programs; designing, building, and experimenting with software tools that predict the deterministic execution times of programs ; refining and testing our new specification method called communicating real-time state machines (CRSMs); constructing software for executing CRSMs, monitoring their behavior using assertions over timed traces of input-output events, and verifying CRSMs; and using CRSMs as a basis for specifying in-the-large real-time components. Two themes of the research are the incorporation of time as a first-class specification and programming object, and the analysis and exploitation of concurrency.
Principal Investigator: Shaw