Use of Formal Methods in Avionics Triggers Interest in Railway

By Yannick Moy | October 21, 2010

I was invited today to give a talk at Fraunhofer FIRST, a German research institute, on Formal Verification in Aeronautics: Current Practice and Upcoming Standard. I told them about the pioneering work done at Airbus, especially related to unit proof to replace unit testing, and about the new version of the DO-178 standard (the ‘C’ version) expected in 2011, which states that formal methods can be used instead of testing.

Contrast what the DO-178B says:

Formal methods are complementary to testing.

to what the (draft of the) DO-178C says:

Formal methods [...] might be the primary source of evidence for the satisfaction of many of the objectives concerned with development and verification

The audience was around 15 people, half of which from the railway industry in Germany, Belgium and Italy. Their reason for coming to this two-day tutorial around the tool Frama-C, developed by CEA LIST and used at Airbus, is that they have watched with increasing interest the advances of formal methods in the avionics industry, and they would like to apply some of it to the railway domain when possible. Very encouraging, and thanks Jens Gerlach from Fraunhofer FIRST for organizing this kind of events!

Posted in Certification, Events | 2 Comments

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

Posted in Agile/Lean Programming, Certification, Open Source, Papers and Slides | Leave a comment

Safety-critical software and formal verification

By Jamie Ayre | September 10, 2010

Below are a couple of links to a paper and an article discussing the formal verification of safety-critical applications.

The first one is an article written by Boris Sedacca in the IET magazine “Verifying safety-critical aerospace and automotive applications” looking at how the current and upcoming Avionics and Automotive standards “aim to improve code verification”.
http://kn.theiet.org/magazine/issues/1013/verifying-safety-1013.cfm

The second one is a paper written by Xavier Leroy who is a member of the team at INRIA working on the CompCert project. “The paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness.”
http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf

Posted in Certification, Related Initiatives | Leave a comment

Integrating Formal Methods into Software for Avionics Certification

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.”
Posted in Certification, In the Press, Open-DO News | Leave a comment

Challenges facing avionics software developers

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.
Posted in Certification, In the Press | Leave a comment

Must-see Videos on Code Verification

By Yannick Moy | August 24, 2010

Rustan Leino, a researcher at Microsoft Research, has started creating a set of videos where he both teaches and demoes how to do code verification with the tools developed at Microsoft Research. This shows how to overcome the difficulties than someone may encounter with every code verification tool, except the GUI is amazingly intuitive (verification in the background while typing, very precise error messages).

No only that, but Rustan also sings and dances… really enjoyable!

Posted in Videos | Tagged , | Leave a comment

Certification Together Conference

By Jamie Ayre | July 26, 2010

According to the website, “The Certification Together International Conference for the Aeronautical Industry is the only event in Europe fully dedicated to System, Software and Hardware certification challenges.”

Looking at the program, a large part of it, as you’d expect, is dedicated to the changes in the upcoming DO-178C standard and how it will affect current certification process and practices. Coupled with these are more practical, hand-on user studies provided by primes and vendors alike.

Cyrille Comar will be giving a talk based around “The challenges of Agile certification” and an update on the Object Oriented Technology (OOT) supplement of DO-178C.

The event will be held in Toulouse, France – Oct 26-28.

Posted in Agile/Lean Programming, Certification, Events, Related Initiatives | Leave a comment

Achieving Embedded Software Safety with Agility

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.

Posted in Agile/Lean Programming, Certification, In the Press | 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.

Posted in Open-DO News, Papers and Slides | 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.

Posted in Agile/Lean Programming, Certification, Papers and Slides | Tagged , , , , | 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