Category Archives: Papers and Slides

Being Elmer Fudd

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

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.
Also posted in Agile/Lean Programming, Certification, Events, Open Source | Tagged , , , , , | Leave a comment

Case Study: Can you afford to ignore formal analysis?

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

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

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

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)

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.

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

The Use of Formal Methods on the iFACTS ATC Project (Neil White)

The next talk in our series from the recent Open-DO Conference is from Neil White, Principal Engineer with Altran Praxis. His talk provides an overview of the formal methods used on the iFACTS project. iFACTS is delivering increased Air Traffic Control capability to the UK.



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

Also posted in Events, Videos | Leave a comment

Agile Methods and Safety-Critical Software (Peter Gardner)

The next talk in our series from the recent Open-DO Conference is from Dr. Peter Gardner. Peter has twenty years experience in languages and software development methodologies and acts as the focal point for UML in Silver Atena. His talk surveys Agile methods and formulates a list of features that occur in these methods, then considers whether each of the features can be applied in the field of safety-critical software development.



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

Also posted in Agile/Lean Programming, Events, Videos | 12 Comments

Open-DO Update (Cyrille Comar)

The next talk in our series from the recent Open-DO Conference is from Cyrille Comar, Managing Director of AdaCore EU, who gives an update on the latest happenings with the Open-DO initiative and talks about AdaCore’s new French government funded project, Hi-Lite, which has the goal of promoting the use of formal methods in developing high-integrity software.



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

Also posted in Events, Open-DO News | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org