Scholarlink

<p>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.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Automated property-based testing from AADL component contracts

  • 期刊论文

  • 发表日期：

    2025年4月23日

查看全文
  • John Hatcliff,
  • Jason Belt,
  • Robby,
  • Jacob Legg,
  • Danielle Stewart,
  • Todd Carpenter

摘要

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.