Abstract:
The DO-178C standard improves upon the previous DO-178B version by better supporting newer concepts in software development processes and methods. The new standard contains a core document and four supplements. The core document is an updated version of DO-178B with clarifications, improvements and many known issues addressed. The supplements clarify certification using object oriented technology and related techniques, model based development and verification, formal methods, and software tool qualification considerations. This paper will discuss the new DO-178C guidance for tool qualification and will present an approach to tool qualification based on iterative and agile development methods. Through this approach tools may be qualified at a lower cost and more importantly re-qualified for new software development environments as tools sets (such as compilers) are updated during the main application’s certified development life span.
In his recent Embedded Computing Design article, Ben Brosgol discusses “Non-intrusive code coverage for safety-critical software” and more specifically how a “tool that derives precise source-level coverage metrics from execution trace data for a non-instrumented program” can really help with DO-178B evidence requirements. Abstract below with a link to the the full article…
Certification standards such as DO-178B for avionics require evidence that the system source code is completely exercised by tests derived from requirements. Traditional tools obtain the coverage data for a test run through code instrumentation, but this complicates analysis since the code being exercised is not the code that will finally execute. A solution to this problem is provided by a combination of two new tools, one for target emulation and one for coverage analysis. GNATemulator translates target object code into native host instructions, with the resulting code running on the host. This approach is efficient (target code is not being interpreted dynamically) and convenient (a significant amount of development can be conducted without an actual target board). Running on an instrumented version of GNATemulator, the GNATcoverage tool non-intrusively provides coverage data at both the source and object levels. At the object code level the tool performs instruction and branch coverage. At the source code level it provides statement coverage, decision coverage, and Modified Condition/Decision Coverage (MC/DC), performing the necessary analysis when MC/DC cannot be deduced from object branch coverage, and fully supports all levels of DO-178B safety certification.
Abtract
“To achieve certification, safety-critical systems must demonstrate compliance with domain-specific standards such as DO-178 for commercial avionics. Developing a certified system consists of various interrelated activities that produce outputs (collections of artifacts) as evidence of successful completion. For example, one of the DO-178 verification activities is a traceability analysis; its output is a report showing that each software requirement is implemented in the source code. Conducting the certification-required activities and producing the artifacts demand a major effort, much more than for conventional Quality Assurance on non safety-critical systems.”
Read the full article.
We learned this week of ImProve, a lightweight DSL intended for building high assurance embedded applications. Developed by Tom Hawkins, the tool is an EDSL that performs formal verification (via. model checking) and code generation. The host language is Haskell; meaning ImProve programs are nothing more than Haskell programs that call the ImProve library API.
ImProve’s semantics are extremely simple:
- It is an imperative language like C or Ada.
- It only has 3 datatypes (bool, int, float).
- There are a total of 16 expression types (add, subtract, AND, OR, etc.).
- Statements consist of variables assignments, conditional “IF” statements, and assertions.
In terms of the ImProve compiler structure, a thin layer of Haskell helps translate ImProve programs down to an intermediate representation, from which programs are verified and C code is generated.
For verification, the IR language is passed to a k-induction model checker (part of the ImProve library), which makes calls down to an SMT solver (currently Yices). ImProve provides assertions statements to capture design intent. Assertions can be seeded with previously proven lemmas to aid verification convergence.
For more information, please visit the project website:
From a talk given at the SPARK User Group 2010 High Assurance Software Symposium, Rod Chapman from Altan Praxis talks about the guiding principles behind PSP (Personal Software Process) and TSP (Team Software Process).
Below are the slides from the recent Couverture project conclusion meeting. Cyrille Comar presented the original needs and goals of the project, the challenges the team came across a long the way, and the main results.
In a paper first published in 2008, Christophe Bertrand and Christopher P. Fuhrman from the Department of Software and IT Engineering, ÉTS, Montreal, Canada, discuss how OpenUP (”a minimally sufficient software development process – meaning that only fundamental content is included”), could be adopted for use in the context of building high-integrity (DO-178B) software.
Abstract:
“Civil avionics software must be certified according to standards mandated by governmental agencies, such as the Federal Aviations Administration in the United States. Typically the certification is done in the context of the DO-178B standard. For companies seeking a first-time certification, preparation for DO-178B can be a daunting challenge. The documentation and planning of high-integrity software is therefore a software engineering problem. As a solution, we consider an open-source derivative of the Unified Process, called OpenUP, as a base process model from which to begin. Because of their importance in the DO-178B standard, software requirement activities are the focus of our study. We show that most of DO-178B’s objectives in this dimension could be supported with activities in OpenUP.”
According to the website, “The Certification Together International Conference for the Aeronautical Industry is the only event in Europe fully dedicated to System, Software and Hardware certification challenges.”
Looking at the program, a large part of it, as you’d expect, is dedicated to the changes in the upcoming DO-178C standard and how it will affect current certification process and practices. Coupled with these are more practical, hand-on user studies provided by primes and vendors alike.
Cyrille Comar will be giving a talk based around “The challenges of Agile certification” and an update on the Object Oriented Technology (OOT) supplement of DO-178C.
The event will be held in Toulouse, France – Oct 26-28.