Formal Verification of Behavioral AADL Models by Stateful Timed CSP

AADL along with its Behavior Annex is an architecture and behavior description language for safety-critical domains, e.g. avionics, aerospace, and defence. In order to formally analyze behavior properties of AADL models, it is necessary to transform the AADL language into formal languages supported by formal verification tools. Moreover, comprehensive formal verification of AADL models highly requires that the transformation supports larger subset of the AADL language, as well as verification tools are able to capture various behavior of AADL, such as concurrency and timing. As an extended communicating sequential process (CSP), stateful timed CSP with its model checker-PAT provide an strongly expressive language and verification tool for real-time systems, distributed systems, and concurrent systems. This paper introduces a model transformation approach from a comparatively complete subset of AADL to stateful timed CSP, in particular supporting major components of AADL Behavior Annex. We propose a comprehensive set of transformation rules for AADL to stateful timed CSP. Then, we perform formal verification in PAT to analyze concurrent behavior properties of AADL models, such as safety, liveness, and trace refinement with various fairness assumptions, in which we consider time capacities, deadlines, periods of AADL threads and durations of AADL processes. As a study case, we develop an AADL model of F-16 'Auto Pilot Controller' and transform the model into Stateful Timed CSP. We specify a set of critical properties of the model and perform formal verification in PAT.