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.
Wed 11 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | |||
13:30 30mTalk | Methodical and Formally Verified Model-Driven Architecture Refactoring ECMFA Lars Fischer Chair of Software Engineering, RWTH Aachen University, Hendrik Kausch RWTH Aachen University, Chair of Software Engineering, Bernhard Rumpe RWTH Aachen University, Max Stachon RWTH Aachen University, Sebastian Stüber RWTH Aachen University, Chair of Software Engineering, Lucas Wollenhaupt Chair of Software Engineering, RWTH Aachen University Link to publication DOI | ||
14:00 30mTalk | On the Use of GPT-4 in the Reverse Engineering of Class Diagrams ECMFA Victor Campanello Chalmers University of Technology, University of Gothenburg, Shariq Shahbaz Chalmers University of Technology, University of Gothenburg, Vladislav Indykov Chalmers | University of Gothenburg, Daniel Strüber Chalmers | University of Gothenburg / Radboud University Link to publication DOI | ||
14:30 30mTalk | Using MDE to support sustainable re-engineering ECMFA Dr Kevin Lano King's College London, Shekoufeh Rahimi University of Roehampton , Zishan Rahman King's College London Link to publication DOI |