Thales develops critical embedded software in C, where full code coverage and rigorous testing are essential to meet regulatory standards. As systems grow more complex, teams increasingly rely on open-source components that have not followed a strict V-model development cycle and are often poorly covered by tests.
Writing tests manually for these components is time-consuming and error-prone. The challenge was to create a tool that could automatically generate comprehensive unit tests while orchestrating multiple advanced testing techniques that are otherwise difficult to use individually or in combination.
Thales selected Titagone for our proven expertise in formal methods, automated testing, and critical systems verification. Our team's deep understanding of symbolic execution, model checking, and program analysis, combined with our experience in aerospace and defense applications, made us uniquely qualified to tackle this challenge. Our ability to design and implement sophisticated tool orchestration while ensuring reliability for safety-critical systems was essential for this mission.
In 2023, Thales partnered with Titagone to develop SeaCoral, a software tool that automatically generates unit tests for C code, orchestrating multiple advanced testing techniques: fuzzing, concolic testing, and model checking. The goal was to maximize code coverage, detect unreachable code, and identify runtime errors, all while producing reports that could be integrated into development workflows.
SeaCoral operates by coordinating multiple analysis tools, ensuring they share consistent assumptions about program inputs, memory structures, and coverage labels. For example, it generates customized harnesses for KLEE, CBMC, and libFuzzer, allowing them to handle symbolic arrays, dynamic memory, and other complex data structures. Advanced orchestration strategies prioritize fast dynamic analyses first, then static coverage tools, and finally precise dead-code detection, optimizing both performance and thoroughness.
The impact of SeaCoral is multifaceted. In projects requiring full coverage, the tool supplements existing test suites with new, automatically generated tests, ensuring that all code paths are exercised. In long-lived applications, these tests guard against regressions as the code evolves.
In continuous integration environments, SeaCoral runs automatically at each build, highlighting runtime errors or dead code as they appear. Beyond safety, it also aids security testing, revealing potential vulnerabilities through systematic exploration of execution paths. The SeaCoral project combines deep research in test generation, formal methods, and practical software engineering, resulting in a robust, extensible, and user-friendly platform that accelerates test generation, improves code reliability, and integrates seamlessly into industrial development pipelines.
Let's discuss how automated test generation can improve your code coverage and software reliability.
Get in Touch