Formal Verification of AADL Specifications in the Topcased Environment


We describe a formal verification toolchain for AADL, the SAE Architecture Analysis and Design Language, enriched with its behavioral annex. Our approach is based on tools that are integrated in the Topcased environment. We give a high-level view of the tools involved and illustrate the successive transformations that take place during the verification process.

In Ada Europe 200914th Ada-Europe International Conference