Many object oriented analysis methods produce several models in order to describe the properties and the behavior of a system from various viewpoints. These multiple model approaches facilitate understanding of the system, since each model describes the different aspect of the system. However, it is quite possible that may exist the inconsistency between models.
In this thesis, we propose methods for checking the consistency between the models based on Object Modeling Technique : the consistency between object model and dynamic model and the consistency between dynamic model and functional model. The object model tends to be specified at a lower level of abstraction than that of the dynamic model, which impedes checking the consistency between them. We resolve this problem by harmonizing the abstraction level of the object model with that of the dynamic model by grouping objects in the object model. Since a function in the functional model is performed through transition-traces in the dynamic model, the semantics of transition-traces should coincide with that of the functional model. The previous works on the consistency checking between dynamic model and functional model impose a restriction that they support no mutual messaging. We present a new method for resolving such a restriction using the symbolic execution.
