Category Archives: Open-DO News

Agile Qualification and the Qualifying Machine

Matteo Bordin presented the Qualifying Machine at the Certification Together Conference 2010 . The Qualifying Machine is an integrated repository to manage qualification (and certification) -oriented artifacts like requirements, test cases, source code and verification reports. Its main goal is to provide an agile framework to cope with end-to-end traceability, incremental certification/qualification and change impact analysis.
Posted in Open-DO News | Leave a comment

Hi-Lite Progress: Discussions on Specification Languages

We had yesterday our first joint meeting in Hi-Lite since the start of the project, 6 months ago. This was the occasion for CEA to present their ideas for E-ACSL (the executable fragment of the ACSL specification language for C) and for us at AdaCore to present our ideas for ALFA (the subset of Ada 2012 that will be suitable for formal verification).

The overall directions have been agreed by all partners. In particular, we agreed on the vision of a product that allows unit testing and/or unit proof on individual functions from a program, depending on the features of C/Ada exercized in the function. This will be a major departure from other formal verification tools and methodologies (SPARK, B method) allowing a finer-grain choice of what should be formally verified and what should be tested.

Discussions on E-ACSL and ALFA are expected to continue on the public mailing list

Posted in Open-DO News | Leave a comment

Integrating Formal Methods into Software for Avionics Certification

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.”
Also posted in Certification, In the Press | 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 Papers and Slides | Tagged , | Leave a comment

XReq Project

XReq – Executable Requirements for DO-178B – is the latest project to join the Open-DO initiative. XReq, first contributed by Sogilis, is a tool designed to help testing and verifying a project. It has been specifically adapted for the DO-178B context but can be used by a much wider audience. To help DO-178B projects, it bring together the tests (HLT/LLT) with their requirements, thus helping traceability of the tests.

For further information, please visit the XReq project page.

Also posted in Certification | Leave a comment

ERTS² conference week

I spent a very interesting week in Toulouse last week. It started with a day of conference in which INRIA research labs showed a host of products and advanced research applicable to the domains of modeling and safety. There was in particular demos of Astrée (static analyzer for C, now sold by AbsInt Gmbh), Frama-C (framework for analyses on C, partner in Hi-Lite) and Alt-Ergo (prover SMT, partner in Hi-Lite).

It continued with the conference ERTS² during 3 days, which gathered many French and European providers and customers of embedded solutions. I’d like to highlight 3 presentations:

Also posted in Certification, Events | 1 Comment

A “Lighter” Introduction to Hi-Lite

The recently launched project Hi-Lite is based on powerful industrial tools that have been developed by the different partners for the last 10 to 25 years. This means in particular that it is not obvious to grasp the “vision” of Hi-Lite without knowing how all these tools work. To share this vision as broadly as possible, we have come up with a “light” (one may even say humorous) introduction to Hi-Lite in which we describe the application of the various tools and techniques that are part of Hi-Lite to a very simple program.
Posted in Open-DO News | Tagged , , , , | Leave a comment

David Crocker’s Verification Blog

In case you missed the very interesting blog that David Crocker of Escher Technologies is writing since January of this year, I have put a link to it in the Blogroll that you find on the right of the Open-DO main page. David’s ArC system reads C code together with annotations written in special macros in order to formally prove properties of C code. Many similarities with Frama-C, yet a different interesting point of view. Plus David’s choice of examples and tone makes it a very nice reading.
Posted in Open-DO News | 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, Papers and Slides, Videos | Leave a comment

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, Papers and Slides | Leave a comment
  • Categories

  • Open-DO Projects

  • Contact

    info @