Creating Better System Models: A Method for Using Compositional Reasoning to Validate Architectures with Assumption/Guarantee Contracts

Formal methods have proved to be a valuable tool for identifying defects early in the development of safety-critical systems. Despite that, several factors have impeded their adoption within the systems engineering community. Some of these include lack of commercially available solutions, poor inte-gration of analysis functionality in existing model-based systems engineering (MBSE) tools, and difficulty interpreting the results of the formal analyses. One such analysis that is popular among pockets within the aerospace community is the Assume Guarantee Reasoning Environment (AGREE), which analyzes Architecture Analysis and Design Language (AADL) models. AGREE is an open-source property-proving model checker that uses compositional reasoning to prove the system composition is valid based on assumptions and guarantees associated with the system com-ponents. The goals of this work are to develop a method for using AGREE in a more widely adopted commercially available tool and to take advantage of MBSE formalisms to better convey the analysis results, especially counterexamples. The hope is that this will increase the use of formal methods by high-assurance systems developers.