Category Archives: In the Press

Software Glitches: Why We Shouldn’t Put Up With Them

Robert Dewar discusses why software glitches are unacceptable in this day and age.

Software Glitches: Why We Shouldn’t Put Up With Them
Posted in In the Press | Leave a comment


An interesting new website added to the family of NASA websites. code.NASA, according the website, NASA “…will continue, unify, and expand NASA’s open source activities. The site will serve to surface existing projects, provide a forum for discussing projects and processes, and guide internal and external groups in open development, release, and contribution.”

More information can be found at:

I particularly like the call for participation – “Will your code someday escape our solar system or land on an alien planet? We’re working to make it happen, and with your help, it will.”

Also posted in Open Source, Open-DO News, Related Initiatives | 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.

Also posted in Agile/Lean Programming, Certification, Open Source | 1 Comment

NASA’s drive towards open source

An excellent interview in Military Embedded Systems this week looking at NASA’s drive towards open source software. Sharon Hess interviews Ray O’Brien, Chief Technology Officer for Information Technology at NASA Ames Research Center. In it, O’Brien discusses NASA’s OSS policy, projects, and the advantages they are seeing from interacting with the OSS community.
Also posted in Open Source | 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.


“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 Agile/Lean Programming, Certification | Leave a comment

Cookbook for Applying Formal Methods in Industry

If you read a bit of French, you’ll be happy to know that Hermes Publishing has just issued the first of a three-volume series on Utilisations industrielles des techniques formelles (use of formal methods in industry). This first volume is concerned with abstract interpretation techniques and tools. As such, we at AdaCore contributed a chapter on the static analyzer CodePeer that we develop. Other chapters describe the use of other tools based on abstract interpretation and formal methods in a broader sense: Polyspace, Astrée, Frama-C, etc. I liked in particular the discussion about the use of formal methods for in DO-178C context, and the combination of formal verification and testing, in chapter 7 by Dassault Aviation Méthodes formelles et conformité au standard DO-178C/ED-12C en aéronautique. We do have solutions in project Hi-Lite to some of the problems they raised.

Here is the book, that you can also find at your preferred web merchant.

The two remaining books on the B methods, Scade, SPARK and others, should be published by the end of 2011. An English version of the three books is expected to be published in 2012.

Posted in In the Press | Tagged , , | 1 Comment

DO-178C Expected for Q1 2011

According to this article, which gives an overview of the changes introduced by this new version of the avionics standard.

I like her presentation of Formal Methods:

Formal methods are a class of mathematically based techniques used for the specification, development, and verification of avionics software. Formal methods tools, for example, are used to represent an aircraft’s mathematically expressed control laws and their translation into software code for the aircraft’s computers. Formal methods can be used to “prove that software is an accurate representation of the mathematical expressions,” Hillary says.

Because formal methods enable software engineers to verify the value of software components, experts say they hope the integrated testing phase will be less manually intensive, Hilderman says.

Formal methods enable software engineers to look at the parts as well as the whole of the code, and help get the software verification process started earlier. Formal methods help verify software components as they are developed, which reduces the need for reverification during integration and testing, which typically cannot start until the software is nearly complete. Under DO-178C, developers will be able to use testing results from earlier in the process as formal results.

Formal methods tools are most helpful with large and complex software programs — 50,000 or more lines of code containing advanced algorithms, Hilderman says. Not many people use them now and it will be some time before they become mainstream.

Also posted in Certification | 2 Comments

Integrating Formal Methods into Software for Avionics Certification

In this recent article published in Defense Tech Briefs, Robert Dewar discusses how integrating formal methods into the software design process can bring better assurance than traditional testing methods. Through the Hi-Lite project, he looks at how testing, static analysis, and formal methods combined could “advance the state of the practice in developing modern avionics systems and other critical software.”
Also posted in Certification, Open-DO News | Leave a comment

Challenges facing avionics software developers

In a recent article “Avionics software programmers challenged by integration, certification, testing issues for software-centric aircraft“, Barry Rosenberg from Avionics Magazine discusses the testing and certification processes used when building these systems.
Also posted in Certification | Leave a comment

Achieving Embedded Software Safety with Agility

In this recently published article in Embedded Technology, Jose Ruiz looks at how Agile methods can be successfully applied when building safety-critical embedded software. He concludes:

“Production of safety-critical systems is typically expensive and not conducive to changes. Agile techniques can help increase the level of automation in production and certification, increasing adaptability to changing requirements and reducing delivery time and cost. These methods are based on iterative and incremental development, verified by continuous and automated tests. This notion can be extended to all certification artifacts to achieve continuous certification.”

To read the full article, please click here.

Also posted in Agile/Lean Programming, Certification | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @