Finding inconsistency for UML-based composition at program level

In this paper, we study how to enforce the composition based on the Unified Modeling Language (UML 2.0) at the program level. We develop a novel technique for automatically detecting the inconsistency for composition between a class diagram and its implementation program using a software model checker. Specifically, given the attributes that are intended to implement composition in a UML class diagram, our approach checks the composition property in two steps. First, our approach systematically generates all valid object diagrams, i.e. valid input program states. Second, after a method to destroy the owner object is called on each object diagram, our approach checks whether all external links to the owned objects have been removed. Central to this approach is how to prune away the large search space that includes all valid input program states.