Object model specifications 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. 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 specification. 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 specification. The design, implementation and analysis of Embee, a prototype runtime conformance checker for Java programs against Alloy object models, is presented.
展开▼
