Supporting Model Refinement with Equivalence Checking in the Context of Model-Driven Engineering with UML-RT

International audienceThrough model refinement, system developers canbuild a system model incrementally and gradually unveil thedetails of the system. While the process of incrementally buildinga model can help developers master the complexity of the system,even small modifications to a model may lead to a loss of initiallypresent desirable behavior and properties. Furthermore, theimpact of such changes on the model behavior becomes difficultto detect once the model size increases. We propose a formalapproach to compare pairs of models in which the second modelis the result of an incremental modification of the first. The resultshave shown that the approach helps verify that the modificationis behavior preserving, i.e., that it is a refinement in the sense ofthe formal methods literature