Summary
This case study presents a pragmatic process for integrating components developed using different verification methods into a single high-integrity software system. It highlights the challenges associated with the verification of software compliance with requirements, particularly when employing a mix of testing, peer reviews, formal verification, and automatic code generation. The study proposes a method that utilizes AADL as a modeling language for system specification and details how to ensure that properties verified for individual components are preserved in their composition. The paper outlines two approaches—top-down and bottom-up—for system development and discusses the importance of formalizing properties in AADL to verify the correctness of component integration. It also compares the proposed approach with existing methods in the field, emphasizing the relevance of design-by-contract features in languages like Simulink and SPARK 2014. Through practical examples, including the Nose Gear Challenge problem, the study illustrates the application of its proposed methodology.
