Checking property preservation of refining transformations for model-driven development

In Model-Driven Software Development, a software product is created through iteratively refined modelling. It is crucial that this process preserves certain desirable properties of the initial model. However, checking this is increasingly difficult as the models are increasingly more refined. We propose an incremental model checking technique to determine the preservation of safety and liveness properties in models of concurrent systems with respect to changes applied on individual processes, formalised as transformations of Labelled Transition Systems. The preservation check involves checking bisimilarity between transformed and new behaviour, and never involves reexploring unchanged behaviour. We prove its correctness and demonstrate its applicability.