Software systems are evolved over time to enhance various qualities of the software system by adopting new technologies and principles. The architecture design is usually required to be migrated from one architectural style to another to support this adoption, while the key functionalities still need to be preserved. This paper presents a formal approach that supports architectural migration. Our approach automates refactoring the architectural design to support the exploitation of emerging technologies such as microservices and blockchain. With our approach, the refactored architectural design can be verified to ensure that the essential functional requirements are still preserved, and the design has complied with the behavioural constraints of new architectural styles. We have evaluated the accuracy and performance of our approach. The results prove that it performs reasonably well.