CAREER: Time and Event Based System Software Construction

Washington University, Saint Louis MO

Investigators

Abstract

CAREER: Time and Event Based System Software Construction Abstract The research will define and develop a novel suite of tools and techniques for verifiable system software construction. Towards that end, this project is investigating (1) formal models based on timed automata for canonical sets of primitive system software mechanisms, (2) algebraic 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) type systems and other techniques for efficient guidance and checking of system software composition and configuration. 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 project makes it easier for a wide audience of designers, developers and testers to specify, implement and verify correct behavior of software systems. The software and educational materials developed under this project are to be released on-line and open-source.