Category Archives: Agile/Lean Programming

Trusting the tools: An agile approach to tool qualification for DO-178C

Ben Brosgol and Greg Gicca look at agility, tool qualification and the new DO-178C standard in this article in Military Embedded Systems.

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.

Full article here.

Also posted in Certification | Leave a comment

Non-intrusive Code Coverage

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.

http://embedded-computing.com/non-intrusive-code-coverage-safety-critical-software

Also posted in Certification, In the Press, Open Source | 1 Comment

Ada Connection 2011 – Real Time Longevity

From the Ada Connection 2011 talks, Frederic Pinot from Ansaldo STS talks about his experiences developing real-time systems for high-speed rail.

Also posted in Events, Videos | Leave a comment

Ada Connection 2011 – Ada Based Automatic Code Generation Tools in the DO178B context »

From the Ada Connection 2011 talks, Jean-Charles Dalbin from Airbus talks about Ada based Automatic Code Generation Tools in DO178B context.

Also posted in Videos | Leave a comment

EE Times Design article – The Big Thaw

Matteo Bordin, Jerome Lambourg, and Ben Brosgol discuss some of the principles behind the Open-DO initiative in an article entitled The “Big Thaw” – An Agile Process for Software Certification for EE Times Design.

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.

Also posted in Certification, In the Press | Leave a comment

ImProving Formal Verification

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:

https://github.com/tomahawkins/improve/wiki/ImProve

Also posted in Certification | Tagged , | Leave a comment

PSP and TSP: Culture and Discipline for High-Assurance Software

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).



View more videos from the SPARK User Group
2010 High Assurance Software Symposium »

Also posted in Events, Videos | Leave a comment

Slides from the Couverture project conclusion meeting

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.
Also posted in Certification, Events, Open Source, Papers and Slides | Tagged , , , , , | Leave a comment

OpenUP and DO-178B development processes

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.”

Full paper:

Towards Defining Software Development Processes in DO-178B with OpenUP

Also posted in Certification, Open Source, Papers and Slides | Leave a comment

Certification Together Conference

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.

Also posted in Certification, Events, Related Initiatives | Leave a comment
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org