Author Archives: Jamie Ayre

SPARK 2014 – Future directions

Stuart Mathews gave this talk at the recent SPARK User Group. In it he presents the next generation of the SPARK language which will extend the range of programs that can be automatically verified and provides an innovative means for combing formal verification and testing.

Posted in Open-DO News | Leave a comment

Directions in Secure Software Development

Rod Chapman, Altran Praxis, gave this talk at the recent SPARK User Group. This talk reflected on our experiences with building secure systems with SPARK and other formal methods, including the lessons learned from the MULTOS CA, Tokeneer and SPARKSkein projects, and the relationship between safety- and security-critical development. In recent years, there has been [...]

Posted in Open-DO News | Leave a comment

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 [...]

Posted in Open-DO News | 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

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 [...]

Posted in Certification, Events | Tagged , , | Leave a 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:

For questions, remarks, [...]

Posted in Related Initiatives | 5 Comments

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 [...]

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 [...]

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”.


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 [...]

Posted in Certification | 1 Comment

Formalization and Comparison of MCDC and Object Branch Coverage Criteria

This paper was presented by Jerome Guitton at the recent ERTS 2012 conference:
This paper presents formal results derived from the COUVERTURE project, whose goal was to develop tools to support structural coverage analysis of unin- strumented safety-critical software. After briefly introducing the project context and explaining the need for formal foundations, we focus on the [...]

Posted in Certification, Open Source, Open-DO News, Papers and Slides | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @