Thalheim, BernhardWang, Qing2025-12-172025-12-1797836422460500302-9743ORCID:/0000-0001-9504-4273/work/162121082https://hdl.handle.net/1885/733795923We develop a theoretical framework for refining transformations occurring in the process of data migration. A legacy kernel can be discovered at a high-level abstraction which consolidates heterogeneous data sources in a legacy system. We then show that migration transformations are specified via the composition of two subclasses of transformations: property-preserving transformations and property-enhancing transformations at flexible levels of abstraction. By defining a refinement scheme with the notions of correct refinements for property-preserving and property-enhancing transformations, we are able to stepwise refine migration transformations and to prove the correctness of refinements. The result of this paper lays down a formal foundation for investigating data migration.14en201110.1007/978-3-642-24606-7_2480455168046