A coverage analysis toolset for safety-critical software projects undergoing a DO-178B software audit process for all levels of criticality.
Standalone forge project to host the qemu part of the Couverture project developments. This essentially consists in adding to qemu capabilities to emit low level traces of the emulated program execution, which Couverture uses to perform coverage analysis without program instrumentation.
A configuration system designed to organize the Software Configuration Management process according to DO-178B and supports full software life cycle
Hi-Lite is a project aiming at popularizing formal methods for the development of high-integrity software.
Nose Gear Challenge Problem
The goal of this project is to consider how/if theorem proving can have any value in providing assurance in the context of DO-178C formal method supplement. The contributors to the project can use the Nose Gear problem example to explain their techniques. Visit the Nose Gear Challenge Problem page on the Open-DO forge.
A code generation and verification framework for heterogenous models.
A lean and agile infrastructure to ease DO-178 tool qualification. An instantiation for GNATcheck is available.
A technology demo of Riposte, a counter example generator for SPARK verification conditions. Visit the Riposte project page on the Open-DO forge.
The project SPARK Formal aims to develop a complete set of semantics of the SPARK language in Coq, for:
- - at the language level, ensuring the absence of ambiguity and the completeness of evaluation rules
- - at the tool level, ensuring the correct insertion of checks in the AST used for compilation and analysis
The formalization of SPARK also paves the way for the creation of proved toolchains for SPARK programs (a.k.a. "certified" toolchains in academia) such as CompCert.
Sparkel is a new parallel programming language inspired by the SPARK subset of Ada, and designed to support the development of inherently safe and secure, highly parallel applications that can be mapped to multicore, manycore, heterogeneous, or distributed architectures.
XReq is a complete tool to bring together HLT and LLT and their requirements. Test cases are written in an English-based formalism and XReq generates test source code. XReq for DO is adapted for the DO178B but can be used independently as well.A full list of the projects on the Open-DO forge can be found here.