Model transformations across views

AbstractModels of software often describe systems by a number of (partially) orthogonal views: a state machine, a class diagram, a scenario might specify different aspects of the one system to be built. Such abstract, multi-view models are the starting point for transformations into platform-specific models and finally the code. However, during these transformations it is usually not possible to keep such a neat separation into different views: the specification language of the target models might not support all such views. The target model, however, still needs to preserve the behaviour of the abstract, multi-view model. Therefore, model transformations have to be capable of moving aspects of the behaviour across views.In this paper, we study model transformations migrating aspects from state-based views (i.e., class specifications with data and methods) to protocol-based views (i.e., process specifications on orderings of methods) and vice versa. The specification languages for these two views are equipped with a joint, formal semantics which enables a proof of behaviour preservation. We consequently derive conditions for our transformations to be behaviour-preserving, where behaviour preservation is characterised by refinement