A Fresh Take on DO-178C Software Reviews
The software review is an essential part of the evidence required for certification according to DO-178C. In this blog post we reflect on the objectives and challenges regarding DO-178C compliance.
7 entries tagged with #Certification
The software review is an essential part of the evidence required for certification according to DO-178C. In this blog post we reflect on the objectives and challenges regarding DO-178C compliance.
We are happy to announce the availability of GNAT Pro for C++, a versatile development environment for bare-metal targets capable of supporting different subsets of the C++ language. It constitutes the best choice for safety-critical bare-metal systems that want to reduce complexity, memory footprint and execution-time overhead, paving the way to software certification. GNAT Pro for C++ targets popular hardware in the avionics, defense, railway, and space domains: PowerPC (32 bits), x86 (64 bits), RISC-V (32/64 bits), LEON3 (32 bits) and ARM (32/64 bits).
AdaCore provides several tools with certification and qualification capabilities, for the rail and avionics industry. Quentin Ochem’s presentation on “Certification and Qualification” at the 2015 AdaCore Tech Days in Boston, Massachusetts provided more information about these two standards, namely DO-178C and EN:50128:2011.
Frederick Pothon of ACG Solutions has recently published a document entitled - Dissimilar tools: Use cases and impact on tool qualification level on the open-DO blog.
Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.
Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.