Validating inter-object interaction in object-oriented designs

Object classes are the building blocks for object-oriented software. Design methodologies have focused on methods, tools and representations to build classes taking advantages of inheritance and encapsulation properties. The guiding principle being that if all classes are correctly constructed a system consisting of objects in these classes will be correct. Efforts to include object constraints in object-oriented programs have not attained the role commensurate with the role invariants play in traditional imperative programs in understanding the programs and in establishing correctness properties. The paper describes use of a model checker to establish the correctness of an object-oriented design.