Runtime Conformance Checking of Objects Using Alloy
Michelle L. Crane, Juergen Dingel · Electronic Notes in Theoretical Computer Science · 2003
Object models are an important part of most object-oriented software development methodologies, where they play a central role during the specification and design phases. However, their usefulness is much more limited during the implementation phase. In this paper, we demonstrate how confidence in source code can be increased by using runtime conformance checking to analyze the code with respect to an object model. More precisely, we use the Alloy Analyzer, developed at MIT, to determine automatically whether the runtime state of a program at certain user-specified locations conforms to a given object model. The design, implementation and evaluation of a prototype runtime conformance checker for Java programs with respect to Alloy object models is described.