Checking strong specifications using an extensible software model checking framework

Abstract

The use of assertions to express correctness properties of programs is growing in practice. Assertions provide a form of checkable redundancy that can be very effective in finding defects in programs and in guiding developers to the cause of a defect. A wide variety of assertion languages and associated validation techniques have been developed, but run-time monitoring is commonly thought to be the only practical solution. In this paper, we describe how specifications written in the Java Modeling Language (JML), a general purpose behavioral specification language for Java, can be validated using a customized model checking framework. Our experience illustrates the need for customized state-space representations and reduction strategies in model checking frameworks in order to effectively check the kind of strong behavioral specifications that can be written in JML. We discuss the advantages of model checking relative to other specification validation techniques and present data that suggest that the cost of model checking strong program specifications is practical for several real programs. © Springer-Verlag 2004.