Want to get involved?
Contactinfo @ open-do.org
Category Archives: In the Press
By Jamie Ayre | January 20, 2014
Robert Dewar discusses why software glitches are unacceptable in this day and age. Software Glitches: Why We Shouldn’t Put Up With Them
By Jamie Ayre | January 5, 2012
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: http://open.nasa.gov/blog/2012/01/04/the-plan-for-code/ 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.”
By Jamie Ayre | November 16, 2011
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.
By Jamie Ayre | October 26, 2011
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.
By Jamie Ayre | September 21, 2011
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.
By Yannick Moy | July 13, 2011
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.
By Yannick Moy | October 22, 2010
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.
By Jamie Ayre | September 6, 2010
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.”
By Jamie Ayre | August 31, 2010
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.
By Jamie Ayre | July 9, 2010
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.