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.
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. Specific technical outcomes of this research have been published in doctoral dissertations by Venkita Subramonian and Terry Tidwell at Washington University in St. Louis, and in peer-reviewed papers that were presented and published at the IPDPS 2006, EMSOFT 2006, OPODIS 2006, and ECRTS 2011 conferences. Further details about this research, and links to publications and dissertations, can be found at www.cse.wustl.edu/~cdgill/CAREER/ (the project web site).
