EMBRAER S.A. - An automated method and toolchain for assessing completeness of requirements-based tests using formal representations

The project addresses the problem of systematically assessing the completeness of requirements-based testing in safety- and mission-critical systems. It proposes an automated method and an integrated toolchain that leverage formal representations of requirements to enable rigorous, traceable, and repeatable completeness analysis. The approach combines requirement formalization (e.g., temporal logics, automata-based models, or contract-based specifications) with automated analysis techniques to derive test obligations, measure coverage with respect to formally defined semantics, and identify gaps between specified behavior and executed tests. The toolchain is designed to integrate with existing development and verification workflows, supporting traceability between requirements, formal models, and test artifacts. The expected outcome is a demonstrably more precise and objective assessment of test completeness compared to conventional coverage criteria (e.g., code-based metrics), thereby improving assurance in verification and validation processes.