Abstract
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.
Cite
CITATION STYLE
Hatcliff, J., Belt, J., Robby, Legg, J., Stewart, D., & Carpenter, T. (2023). Automated Property-Based Testing from AADL Component Contracts. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 14290 LNCS, pp. 131–150). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-43681-9_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
