Methodical and Formally Verified Model-Driven Architecture Refactoring.

Verification is necessary to ensure the correctness of safety-critical software systems.When developing such systems in an agile way, it is important to guarantee that the correctness still holds after refactoring, e.g., no new behavior is introduced.To support the iterative development of such systems, we have translated refactoring patterns based on syntactic transformations of pipeline architectures to Isabelle, an interactive theorem prover.Isabelle is employed to verify refactoring steps performed on component-and-connector architectures transformed from SysMLv2 models.In particular, we have translated several verified architecture refactoring patterns to Isabelle.The application of the development patterns is demonstrated by a case-study in which a secure communication channel is added to an architecture modeled in SysMLv2.We envision that by utilizing model-driven system engineering in conjunction with development patterns and tool-supported formal behavior verification, engineers can effectively improve and refactor existing systems without compromising previously certified correctness results.