C2AADL_Reverse: A model-driven reverse engineering approach to development and verification of safety-critical software

The safety-critical system communities have been struggling to manage and maintain their legacy software systems because upgrading such systems has been a complex challenge. To overcome or reduce this problem, reverse engineering has been increasingly used in safety-critical systems. This paper proposes C2AADL_Reverse, a model-driven reverse engineering approach for safety-critical software development and verification. C2AADL_Reverse takes multi-task C source code as input, and generates AADL (Architecture Analysis and Design Language) model of the legacy software systems. Compared with the existing works, this paper considers more reversed construction including AADL component structure, behavior, and multithreaded run-time information. Moreover, two types of activities are proposed to ensure the correctness of C2AADL_Reverse. First, it is necessary to validate the reverse engineering process. Second, the generated AADL models should conform to desired critical properties. We propose the verification of the reverseengineered AADL model by using UPPAAL to establish component-level properties and the Assume Guarantee REasoning Environment (AGREE) to perform compositional verification of the architecture. This combination of verification tools allows us to iteratively explore design and verification of detailed behavioral models, and to scale formal analysis to large models. In addition, the prototype tool and the evaluation of C2AADL_Reverse using a real-world aerospace case study are presented.