DO-330/ED-215 Benefits of the New Tool Qualification Document

As part of the DO-178C/ED-12C revision effort, a new document Software Tools Qualification Considerations (DO-330/ED-215) was developed. Its goal is both to replace the software tool qualification guidance of DO-178B/ED-12B and also to enable and encourage the use of this “mature” guidance outside the airborne domain. Since it may be used independently, DO-330/ED-215 is not considered as a supplement to DO-178C/ED-12C; it is thus titled differently from the specialized technology supplements.

The purpose of this document is to describe how DO-330/ED-215 impacts the current tool qualification approach of DO-178B/ED-12B and how it provides more relevant guidance for both tool users and tool providers.

We first review the rationale for a Tool Qualification document. But before the application of DO-330/ED-215, a fundamental pre-condition is to establish for the project the tool qualification criteria and the Tool Qualification Levels (TQLs). As an example, we show how DO-178C/ED-12C determines the criteria and TQLs for the airborne domain. In this domain, the criteria are based on the possible impact of a tool error on the software life cycle processes.

We then highlight the main impact of DO-330/ED-215 on current practice, and provide the relevant information to help the reader to apply this new guidance.

Some supporting information is provided in an appendix of DO-330/ED-215. We describe one of the most important topics, addressing the possible certification credit when using a qualified AutoCode Generator (ACG).

The author, Frédéric Pothon ACG Solutions, and several of the contributors and reviewers participated in the DO-178C/ED-12C working group and subcommittees.

Download document.

© Frédéric Pothon, 2012
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Posted in Open-DO News | Leave a comment

Future Version of SPARK Will Be Based on Ada 2012

At the SPARK User Day yesterday in Bath, Altran-Praxis and AdaCore announced that the SPARK language will undergo a major transformation, to both extend the subset of Ada included in SPARK, and to use the new specification features of Ada 2012 instead of special comments like in today’s SPARK language. This is only fair that, SPARK annotations being the source of inspiration for many of the new specification features in Ada (pre- and postconditions, quantified expressions, etc.), their executable Ada version is now included in SPARK. This future version is expected to be released Q1 2014.

This is something we have been working on for almost 3 years now, between Altran-Praxis and AdaCore, inside the Hi-Lite project. We have been able to show that, not only we can extend the range of programs which can be proved automatically correct with respect to their specification, but we can combine much more easily testing and formal verification than what was considered possible until now.

Given the results achieved already, some (like the Microsoft researcher Rustan Leino who asked me this question at the SPARK User Day) could wonder why we don’t plan to release a product sooner. This was answered by a current SPARK customer, Robert Dorn from Secunet, who said that they want “first, that the future SPARK language and toolset allows them to express and prove as much as the existing one, and only then, that it extends the language and provides improved and new tools”. The work done in Hi-Lite is mostly concerned with automatic proof of functional properties. We are now working also on the expression and verification of data and information flow properties that are so important for many SPARK users.

We will continue to provide GPL releases of prototypes of these future tools to the community in 2013.

Posted in Events, Open Source | Tagged , , | Leave a comment

DO-178C/ED-12C vs DO-178B/ED-12B: Changes and Improvements

This document identifies all the changes in the new release DO-178C/ED-12C, explains their rationale, and highlights the impact of these changes on the various software processes. The PDF can be downloaded here.

© Frédéric Pothon, 2012
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 Unported License.

Posted in Certification, Papers and Slides | Leave a comment

Use of formal methods in critical systems conference

This conference will take place in Toulouse on November the 12th. It is in French as is the announcement providing more details below:

Les animateurs du DAS Systèmes Embarqués, avec le soutien du thème IFSE du RTRA AE/SE, ont le plaisir de vous annoncer la programmation d’un cycle de conférences techniques sur les méthodes formelles de développement. Non, ne partez pas tout de suite : les méthodes formelles sont faites pour vous !

Ces méthodes ne sont pas assez connues mais ont un potentiel énorme pour faire progresser la productivité ET la qualité intrinsèque des développements de logiciels embarqués et de leurs outils de développement et de vérification. Et elles ne sont pas si difficiles à mettre en œuvre : certains l’ont déjà fait, avec succès, pourquoi pas vous ?

Nous vous proposons donc un cycle de conférence/forum pour vous présenter bien sûr les fondements théoriques de ces méthodes, mais surtout faire un état de l’art et de la pratique, démystifier, échanger, et pourquoi pas monter ensemble des projets pour “passer à l’acte” ? Les intervenants seront à la fois des scientifiques et universitaires les plus compétents dans ces domaines et des utilisateurs “de terrain” qui ont déjà pratiqué ces méthodes et vous livreront leurs retours d’expérience.

La première conférence de ce cycle aura lieu le mardi 13 Novembre 2012 à l’IAS, 23 Avenue Edouard Belin, Toulouse, sur le thème de “l’Utilisation des méthodes formelles dans les systèmes critiques”.

Read More »
Posted in Certification, Events | Tagged , , | Leave a comment

GNATprove Distinguished at VerifyThis Competition

I participated last week in the VerifyThis Verification Competition, which took place on Thursday afternoon during the Formal Methods 2012 conference in Paris. The goal was to apply verification tools to three small challenge programs, to compare approaches and learn from each other’s tools.

I used Ada 2012 as a programming and specification language (using preconditions and postconditions to specify contracts for subprograms) and our prototype GNATprove, a proof tool developed in project Hi-Lite, to formal verify that the code implements its contract and does not raise run-time errors (integer overflows, array index out of bounds, etc.) I completed challenge 1 and I did a part of challenge 2, but I had not enough time to complete it or start on challenge 3.

The competition was followed on Friday by a very interesting explanation session where each team showed how it addressed the problems with its tools. It was particularly interesting to see different solutions from teams using the same language (for example, the two teams using Why3 had quite different solutions for challenge 2), as well as the interaction between the user and the proof tool in KIV, KeY, Why3, etc. I think the problems and their solutions will be added soon to the VerifyThis repository, but if you cannot wait, you can also ask the organizers for a tarball of the submissions.

To come to the title of this post, the organizers awarded a distinction to GNATprove for its integration of proving and run-time assertion checking, of which I’m very proud. As I explained them, this integration was essential in helping me during the competition:

  • For the first problem, I was stuck with a postcondition that I could not prove, and I did not manage to figure out why. So I decided to write a small test to make sure at least that the code and the contract were not contradictory. I executed it, and it raised an exception saying the postcondition was wrong! (because Ada 2012 contracts are executable, the compiler can transform them into run-time assertions, including quantifiers that are transformed in loops) It was then easy to pinpoint the root cause of the problem, the use of “<" instead of "<=" in the test of the main loop.
  • For the second problem, I decided to implement the iterative version of the algorithm, which is more complex to specifiy and verify than the recursive one, but also more representative of critical embedded software. The algorithm is divided in two passes, each one performing two nested loops on the input array, with loop invariants to write for the proof to go through. Being able to execute these loop invariants as regular assertions made me quite confident that I had not written wrong assertions, before I even start proving something.

Hope to see even more participants at the next software verification competition, either VSTTE’s one or VerifyThis!

Posted in Events | Tagged , , , , | 1 Comment

GNATprove tool available

We are happy to announce the first release of GNATprove. This tool is used for formal verification of Ada programs and is being developed as part of the Hi-Lite project. We provide binary distributions for x86 linux, x86 windows and x86-64 bit linux. More details can be found on the following page:

http://www.open-do.org/projects/hi-lite/gnatprove/

For questions, remarks, or issues please contact us on hi-lite-discuss@lists.forge.open-do.org

Posted in Related Initiatives | 5 Comments

ESA is Funding Students on Open-Source Projects this Summer

The European Space Agency is reediting its SOCIS initiative this year. Open-source projects can submit proposals, and ESA will fund between 20 and 25 students to work during two months on these projects.

We submitted a project to extend our work on standard containers adapted to formal verification. Submit yours by July 15th!

Posted in Open Source, Related Initiatives | Leave a comment

Safe and reliable embedded linux programming

Dr José Ruiz gave this talk at yesterday’s Embed with Linux conference in Lorient, France. The talk provides an overview of techniques to design and implement reliable embedded applications. The goal is to achieve safe and analyzable behavior by construction, including handling parallel multiprocessor systems in an efficient and predictable way. The means to attain this objective is to statically configure the application to run on embedded linux platforms, and then to use run-time support to enforce constraints imposed to the system.

Posted in Certification, Events, Papers and Slides | Leave a comment

Hi-Lite team paper at FM 2012

The 18th edition of the International Symposium on Formal Methods organized by Formal Methods Europe will take place at the CNAM in Paris this August. A paper on the work being undertaken by the Hi-Lite team on “Maximal and Compositional Pattern-Based Loop Invariants” will be presented there.

Below is the abstract:

“We present a novel approach for the automatic generation of inductive loop invariants over loops manipulating arrays. Unlike most existing approaches, it generates invariants containing disjunctions and quantifiers, which are rich enough for proving functional properties over programs which manipulate arrays. Our approach does not require the user to provide initial assertions or postconditions. It proceeds by recognizing through static analysis simple code patterns that respect stability properties on accessed locations, on an intermediate representation of parallel assignments. We associate with each pattern a formula that we prove to be a so-called local invariant, and we give conditions for local invariants to compose an inductive invariant of the complete loop. We also give conditions over invariants to be locally maximal, and we show that some of our pattern invariants are indeed maximal.”

Posted in Events, Related Initiatives | Tagged , , | Leave a comment

Excellent paper on avionics software certification

John Rushby from the SRI International Computer Science Library has written a very interesting paper considering the “New Challenges In Certification For Aircraft Software”.

Abstract:

We outline the current approach to certification of aircraft software, and the role of the DO-178B guidelines. We consider evidence for its effectiveness and discuss possible explanations for this. We then describe how changes in aircraft systems and in the air traffic system pose new challenges for certification, chiefly by increasing the extent of interaction and integration.

The full paper can be found at http://www.csl.sri.com/users/rushby/papers/emsoft11.pdf
Posted in Certification | 1 Comment
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org