|
In this paper, we present a type system that is equivalent to model checking. We work with a simple model checking problem, namely, deadline analysis: for an interrupt-driven program, will every interrupt be handled within the deadline? For the interrupt calculus of Palsberg and Ma, we construct finite-state models of programs that enable straightforward model checking for deadline analysis. We then present a type system which type checks exactly those programs that are accepted by the model checker. We use singleton types and, more significantly, intersection and union types containing information about time. Our result sheds light on the relationship between type systems and model checking, and it provides a means of explaining to the programmer why a run of a model checker succeeded and found no bugs. The reason is that the proof of equivalence is constructive and therefore enables type inference by model checking. Thus, a tool can output a version of the program that is annotated with timing information.
This M.S. thesis from Purdue University was announced on the TYPES forum. I don't have the time to read it at the moment but it sure sounds interesting.
Posted to Software-Eng by Ehud Lamm on 7/26/03; 4:34:55 AM
|
|
A Type System Equivalent to Model Checking
