Project detail

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

Duration: 1.9.2026 — 1.9.2028

Funding resources

Neveřejný sektor - Přímé kontrakty - smluvní výzkum, neveřejné zdroje

On the project

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.

Description in Czech
Projekt se zaměřuje na systematické posuzování úplnosti testování založeného na požadavcích v bezpečnostně a provozně kritických systémech. Navrhuje automatizovanou metodu a integrovanou sadu nástrojů využívající formální reprezentace požadavků pro přesnou, trasovatelnou a opakovatelnou analýzu úplnosti testů. Přístup kombinuje formalizaci požadavků (např. pomocí temporálních logik, automatových modelů či kontraktových specifikací) s automatizovanými analytickými technikami pro odvozování testovacích povinností, měření pokrytí vzhledem k formálně definované sémantice a identifikaci mezer mezi specifikovaným chováním a realizovanými testy. Navržená sada nástrojů je koncipována s ohledem na integraci do existujících vývojových a verifikačních procesů a podporuje trasovatelnost mezi požadavky, formálními modely a testovacími artefakty. Očekávaným přínosem je přesnější a objektivnější hodnocení úplnosti testování ve srovnání s tradičními metrikami založenými na kódu, což přispívá ke zvýšení důvěryhodnosti procesů verifikace a validace.

Keywords
requirements-based testing, test completeness, formal methods, formal specification, requirements engineering, model-based testing, coverage criteria, traceability, automated verification, dependable systems

Key words in Czech
testování založené na požadavcích, úplnost testů, formální metody, formální specifikace, požadavkové inženýrství, modelově orientované testování, kritéria pokrytí, trasovatelnost, automatizovaná verifikace, spolehlivé systémy

Default language

English

People responsible

Smrčka Aleš, Ing., Ph.D. - principal person responsible
Fiedor Jan, Ing., Ph.D. - fellow researcher
Jírovec Martin, Ing. - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher

Units

Department of Intelligent Systems
- responsible department (5.5.2026 - not assigned)
Department of Intelligent Systems
- beneficiary (1.9.2026 - 1.9.2028)

Responsibility: Smrčka Aleš, Ing., Ph.D.