Category Archives: Papers and Slides

Prove Your Plane Now!

By Yannick Moy | January 13, 2012

The DO-333 is now available! (ok, that’s not free: 215$ for an electronic version, or 300$ for a hard copy, pfew!)

Under this amazingly explicit name is hiding the formal methods supplement for DO-178C. Or, said otherwise, the document that allows you, as a developer of avionics software, to replace tests/reviews/analyses by formal methods. Or you, as a provider of techniques and tools for formal methods, to find customers in the avionics market. Ah yes, because the new version of the certification standard for avionics software, DO-178C, has been also issued at the same time. So that starts today!

Here is what the abstract of this doc says:

This supplement identifies the additions, modifications and substitutions to DO-178C and DO-278A objectives when formal methods are used as part of a software life cycle, and the additional guidance required. It discusses those aspects of airworthiness certification that pertain to the production of software, using formal methods for systems approved using DO-178C.

Formal methods are mathematically-based techniques for the specification, development and verification of software aspects of digital systems. The mathematical basis of formal methods consists of formal logic, discrete mathematics and computer-readable languages. The use of formal methods is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to establishing the correctness and robustness of a design.

Also posted in Certification, Open-DO News | Tagged | Leave a comment

Best Paper Award for Results of Verification Competition

By Yannick Moy | June 30, 2011

Last year, the conference VSTTE 2010 organized a competition of software verification systems (language + tools), to improve understanding of each system’s pros and cons. Rod Chapman from Altran Praxis participated with the SPARK language and toolset, and solved the first problem even beyond what the subject asked. We have since provided solutions in SPARK to all five problems, like other teams, which formed the basis for a report that you can find on this page.

This report was deemed important enough by the organizers of the Formal Methods conference 2011 that they have granted it the best paper award.

Furthermore, the page of the competition contains an archive with all solutions in many different languages and systems… you can even DIY!

Also posted in Certification, Events | 1 Comment

Language Vulnerabilities for Dummies

By Yannick Moy | June 29, 2011

In case you do not know the series of books “for Dummies”, its principle is to explore a subject from the ground up, with rich explanations and examples for non-experts. That’s in my view a valid alternative title for the recently published “Guidance to Avoiding Vulnerabilities in Programming Languages through Language Selection and Use”. Rich (around 70 vulnerabilities explored) + detailed (130 pages!) + accessible (it contains the best discussion I’ve read of unspecified/implementation-defined/undefined behavior).

The ISO/IEC committee has produced here a language-neutral evaluation of the ways in which a language may “come in the way”, and how to avoid traps and pitfalls either upfront (in language design) or in the field (through coding standards and use of static analysis tools). This is a must-read for anyone whose task is to establish coding guidelines, recommend the usage of a static analysis tool, or choose a programming language for some project.

While Ada and SPARK naturally stand as the languages with fewer vulnerabilities, it also shows the many uses of static analysis tools, from coding standard checking (like GNATcheck) to static analysis (like CodePeer) and formal proof (like SPARK toolset). The recommendations also match well the restrictions for the Alfa subset of Ada that we are defining in project Hi-Lite. (See for example the discussion of aliasing in section 6.39 “Passing Parameters and Return Values”.)

Also posted in Certification | 2 Comments

Being Elmer Fudd

By Yannick Moy | March 31, 2011

Ever found yourself in an extreme stressed state because of some bugs* escaping you? Then you know how it feels to be Elmer Fudd. Not a typical hero, never victorious in his hunt. So it feels being a software engineer. A new episode in this tragicomedy is a paper by Yang et al. from Uni Utah that will be presented at PLDI conference this year.

In this paper, the authors report on 3 years looking for bugs in C compilers. They generated random compliant ANSI C programs, which all C compilers should compile to a program computing the same values, and compared the results of various C compilers on the generated programs. They found 325 bugs, 8 of which they present in a few lines in the paper. Really savory to see how logic defeats man. In case you chill like me over these bug stories, you can read some I wrote at Microsoft and at AdaCore.

The light in the dark comes from a little known C compiler, CompCert whose middle-end successfully defeated the repeated attacks (6 CPU-years!) of the researchers. Guess what? It is written in Coq, a formal language, which allowed proving its correctness. Also interesting is the fact that even CompCert had bugs in its non formally verified parts, like the parser, where it makes sense to have testing in place.

* bunny of course

Also posted in Certification, Open-DO News | Tagged , | Leave a comment

Slides from the Couverture project conclusion meeting

By Jamie Ayre | February 23, 2011
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.
GNATcoverage/GNATemulator launch
View more presentations from AdaCore.
Also posted in Agile/Lean Programming, Certification, Events, Open Source | Tagged , , , , , | Leave a comment

Case Study: Can you afford to ignore formal analysis?

By Yannick Moy | December 6, 2010

This is a title I’d like to reuse some day for a case study in Hi-Lite, but right now it is the title of a very interesting paper published by EE Times: people from Alcatel-Lucent formally verified many properties of an ASIC design in a large communication system.

What is stricking is the similarity of the findings and the challenges with what we do in Hi-Lite, despite the very different nature of the properties verified in hardware and in software, and the different techniques involved. Pages 3 and 4, they detail the additional errors found by formal verification on a codebase already simulated, with actual examples of what simulation missed and why. Very instructive. Which leads them to propose to bring together simulation and formal verification on page 5.

Interestingly, the difficulties to bring these two worlds together are the same as the ones in software: different semantics in simulation and formal verification (ex 1 p 5) and non-executable annotations (ex 2 p 5). Good thing that we insisted on the same semantics in Hi-Lite for execution and formal verification, as well as executable annotations!

Also posted in Certification, Open-DO News | Tagged , , | Leave a comment

OpenUP and DO-178B development processes

By Jamie Ayre | October 4, 2010

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

Embedded Contract Languages by Microsoft Research

By Yannick Moy | June 9, 2010

People from the group developing Spec# at Microsoft Research finally published an article on their new Code Contracts approach.

Chosen excerpts: “embedding of contracts as code is a better approach”; “The language of conditions is just the language of expressions in the programming language used”; “ForAll and Exists that work over integer ranges and collections”; “Any methods called from within contract expressions should be pure methods”; “Runtime contract checking is particularly effective in conjunction with automated testing”; “generating good documentation from the embedded contracts is a key scenario”.

And the conclusion: “Since contract expressions are compiled by the existing compiler, the typical problem of having the specifications and the code drift apart due to edits, refactoring, etc., is avoided.”

All of this supports the vision of project Hi-Lite, and provides valuable experience reports which should inspire us in Hi-Lite.

Also posted in Open-DO News | Tagged , | Leave a comment

Couverture paper presented at ERTS² 2010

By Jamie Ayre | June 8, 2010

At the recent ERTS² 2010 conference held in Toulouse, Thomas Quinot presented a paper entitled

“Object and Source Coverage for Critical Appl ications with the Couverture Open Analysis Framework“.

It presents the Couverture approach to object and structural coverage analysis for certified safety-critical applications, in particular in the context of DO-178.

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

Formal Method for Avionics Software Verification (Hervé Delseny)

By Jamie Ayre | April 28, 2010

The next talk in our series from the recent Open-DO Conference is from Hervé Delseny, an expert in Avionics Software Aspects of Certification at Airbus. In his talk he gives examples of Airbus’ use of Formal Methods to verify avionics software, and summarises the integration of Formal Methods in the upcoming ED-12/DO-178 issue C.



You can also view the presentation slides if you want to follow along.

Formal Method for Avionics Software Verification
View more presentations from AdaCore.
Also posted in Events, Open-DO News, Videos | Leave a comment

  • Categories

  • Open-DO Projects

    Agile
    Couverture
    GeneAuto/Ada
    HiberSource
    Hi-Lite
    Project P
    The Qualifying Machine
    XReq

  • Want to get involved?

    The Open-DO Forge

  • Contact

    info@open-do.org