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.

This entry was posted in Certification, In the Press. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.


  1. foobar
    Posted October 28, 2010 at 13:53 | Permalink

    Does anyone have any knowledge of what object oriented features the current draft allows?

  2. Yannick Moy
    Posted October 28, 2010 at 14:08 | Permalink

    The OO Supplement discusses general concepts of OO languages, like dispatching, hierarchies of classes, and automatic memory management. I believe it does not disallow any specific feature, but rather it mandates that some verifications are done to ensure type consistency: for example, the Liskov Substitution Principle should be obeyed by derived types. (weakest preconditions, strongest postconditions, constraints on exceptions raised, etc)

Post a Comment

Your email is never published nor shared. Required fields are marked *

  • Categories

  • Open-DO Projects

  • Contact

    info @