Automated Property-Based Testing from AADL Component Contracts

Effective and scalable quality assurance techniques are essential for realizing formal model-based development techniques for high-assurance systems. In this paper, we present the GUMBOX property-based testing framework for the SAE standard Architecture and Analysis Definition Language (AADL) integrated with HAMR AADL code generation tool chain. In GUMBOX, automated testing infrastructure for AADL component application code is automatically generated from AADL models and formal specifications written in the GUMBO contract language. This testing framework complements our previous work on using code-level symbolic execution to verify that component source code conforms to model-level GUMBO contracts, and it allows developers to switch between using testing and formal verification with specifications derived from a common contract language. We describe how the GUMBOX framework is incorporated in continuous integration infrastructure with parallel and distributed execution of tests in industrial workflows.