Methodical and Formally Verified Model-Driven Architecture Refactoring

By: Lars Fischer, Hendrik Kausch, Bernhard Rumpe, Max Stachon, Sebastian Stüber, Lucas Wollenhaupt

Abstract

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.

Keywords

Architecture Refactoring, Development Pattern, Formal Verification, Theorem Proving, Model-Driven, SysML.

Cite as:

Lars Fischer, Hendrik Kausch, Bernhard Rumpe, Max Stachon, Sebastian Stüber, Lucas Wollenhaupt, “Methodical and Formally Verified Model-Driven Architecture Refactoring”, Journal of Object Technology, Volume 24, no. 2 (May 2025), pp. 2:1-14, doi:10.5381/jot.2025.24.2.a13.