CAREER: Time and Event Based System Software Construction

NSF Support

This research has been supported by the National Science Foundation, grant CCF-0448562.

Project Description

The goal of this research has been to define and develop a novel suite of tools and techniques for verifiable system software construction. Towards that end, this project has investigated (1) formal models based on timed automata for canonical sets of primitive system software mechanisms, (2) representations of how automata for primitive mechanisms can be composed to form more complex mechanisms that are prevalent in current system software practice, and (3) techniques for efficient guidance and checking of system software behavior. This approach allows system developers to leverage application-specific constraints on the timing and ordering of system events, to guide composition of new mechanisms and customization of previously composed mechanisms. The aim of this project is to make it easier for a wide audience of designers, developers and testers to specify, implement and verify correct behavior of software systems.

Project Participants

Christopher D. Gill, now Professor of Computer Science and Engineering at Washington University in St. Louis, served as Principal Investigator for this research.

Robert Glaubius contributed to this research as a post-doctoral researcher.

Doctoral students at Washington University in St. Louis who have contributed to this research include Venkita Subramonian, Terry Tidwell, and Huang-Ming Huang.

Colleagues at other universities with whom we have collaborated based on the results of this research include:

Invited Colloquia and Master Classes at Washington University

Doctoral Dissertations

Doctoral Dissertation Proposal




A fundamental and fine-grained set of models is needed to be able to uncover subtle safety and timing errors introduced by interference between application computations, particularly in the face of alternative concurrency and dispatching strategies in the middleware layer. To address this need, we have made several contributions in the research so far: (1) developing the models themselves, (2) identifying and developing refinements to the models to increase their fidelity to the middleware domain and to reduce the cost of checking them, and (3) applying our models to verification of properties in several different application and protocol scenarios.