Methodical and Formally Verified Model-Driven Architecture Refactoring.

The Journal of Object Technology, vol. 24, pp. 2:1

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.

Authors 6

1. Lars Fischer Aachen Software Engineering

   RWTH Aachen University

   Affiliation as printed

   Software Engineering , RWTH Aachen University , Germany

2. Hendrik Kausch Aachen Software Engineering

   RWTH Aachen University

   Affiliation as printed

   Software Engineering , RWTH Aachen University , Germany

3. Bernhard Rumpe⋆ Aachen Software Engineering

   RWTH Aachen University

   Affiliation as printed

   Software Engineering , RWTH Aachen University , Germany

4. Max Stachon Aachen Software Engineering

   RWTH Aachen University

   Affiliation as printed

   Software Engineering , RWTH Aachen University , Germany

5. Sebastian Stüber Aachen Software Engineering

   RWTH Aachen University

   Affiliation as printed

   Software Engineering , RWTH Aachen University , Germany

6. Lucas Wollenhaupt Aachen Software Engineering

   RWTH Aachen University

   Affiliation as printed

   Software Engineering , RWTH Aachen University , Germany