Model Driven Engineering (MDE) aims to expedite the software development process by providing support for transforming models to running systems. Many modeling tools provide forward engineering features, which automatically translate a model into a skeletal program that developers must complete. Inconsistencies between a design model and its implementation, however, can arise, particularly when a final implementation is developed dependently on the code from which it was generated. Manually checking that an implementation conforms to its model is a daunting task. Thus, an MDE tool that developers can use to check that implementations conform to their models can significantly improve a developer's productivity. This paper presents a model-based approach for testing whether or not an implementation satisfies the constraints imposed by its design model. Our model-based testing approach aims to efficiently reduce the test input space while supporting branch coverage criteria. To evaluate the approach's ability to uncover inconsistencies, we developed a prototypical tool and applied it to the Eclipse UML2 projects. We were able to uncover inconsistencies between the models and their implementations using the tool.

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.