With the success of model-driven development as well as component-based and service-oriented systems, models of software architecture
are key artefacts in the development process. To adapt to changing requirements and improve internal software quality such
models have to evolve while preserving aspects of their behaviour.
To avoid the costly verification of refactoring steps on large systems we present a method which allows us to extract a (usually
much smaller) rule from the transformation performed and verify this rule instead. The main result of the paper shows that
the verification of rules is indeed sufficient to guarantee the desired semantic relation between source and target models.
We apply the approach to the refactoring of architectural models based on UML component, structure, and activity diagrams,
with using CSP as a semantic domain.
Keywords Service Oriented Architecture - UML - Refactoring - Graph Transformation - CSP