Using Formal Verification in the Landing Field

An article which I co-authored was just published in the May-June special issue of IEEE Software on Safety-Critical Software. It’s called Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, and it talks about how to use formal verification instead of testing for software in civilian airplanes (for which DO-178C applies). It is based on the experience of Airbus and Dassault-Aviation in the application of formal verification with the Frama-C platform.

We describe:

  • What the avionics certification standard DO-178C asks in replacement for test coverage, which does not apply when one uses formal verification instead of testing.
  • How formal verification tools can help with these alternate objectives.
  • The solutions that Airbus and Dassault-Aviation have implemented to cover these objectives.

We’ll be happy to get some feedback from others! Please comment. This paper is copyrighted by IEEE, and reproduced here with their permission. You can also access it on IEEE Software website.

Posted in Papers and Slides | Tagged , | 1 Comment

GNATprove Takes the Train

David Mentré from Mitsubishi Electric R&D Centre Europe has produced a very interesting report on his use of GNATprove (the formal verification tool we develop for the next version of SPARK) on a case-study from the Open-ETCS European project, to develop the tools for the future European Train Control Systems.

Although David asked me to mention this is highly experimental (neither fully proved nor fully tested), I think it shows quite well what one can do with formal verification. The report contains inlined code showing how some units were specified using preconditions/postconditions and annotated with assertions for proofs. You can also download the code from github, or browse it online.

David will present this model at an internal Open-ETCS meeting next Monday, I’ll ask him to post the conclusion of his presentation!

Posted in Open-DO News | Tagged , , | 2 Comments

Integrating Proof and Testing in Verification Strategies for Safety Critical Systems

This talk was given by Cyrille Comar at the recent SPARK User Group. This talk reviews the prominent place and role testing holds in Safety Standards. It compares the strengths and weaknesses of testing with an alternative verification technique based on formal methods. It then explores specific instances where a combination of both approaches makes sense and can bring significant cost savings, without forcing dramatic changes in internal development procedures.

Posted in Open-DO News | 2 Comments

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 a huge resurgence in interest in static analysis of software, largely driven by the perception of “security vulnerabilities” in both specific systems and programming languages in general. This talk also considered the trends emerging in this market, both good and bad, and proposed one view of what the future might hold for secure systems development.

Posted in Open-DO News | Leave a comment

Axioms and Proofs: When Less is More

In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so there is a problem with the code or the assertions in the program). The reality is that the prover may take a long time to reply yes/no, and that in some cases it just replies I don’t know!

A promising approach to help automatic provers answer more quickly is to reduce the size of the formula. Typically, this formula contains thousands of axioms defining all relevant symbols from the program (functions, types, constants), as well as describing the context in which the formula should hold (typically a path or set of paths through a function, as produced by a verification condition generator). Researchers have proposed strategies to start with a small subset of these axioms, and incrementally grow it until a proof is found. At AdaCore, Duc Hoang is ending today a 6 months internship on that subject.

We have devised a strategy based on definition links, as in the work of Josef Urban (”An overview of methods for large-theory automated theorem proving”) and SInE, with a graph-based approach, similar to the work of Couchot et al. (”A graph-based strategy for the selection of hypotheses” & “Graph Based Reduction of Program Verification Conditions”).

This work is publicly available, if others want to try it out (main switch is -autoselect), in the git repository for our version of Alt-Ergo:

git clone

We had a discussion a few days ago on this subject and others related to Alt-Ergo with CEA-LIST research lab and OCamlPro company, both interested in a shared development of Alt-Ergo. If you are also interested in joining this effort, contact us at AdaCore.

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

not Taking Assumptions for Granted

The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove. Assumptions may either be related to the proof of a single function (like “this other function called should respect its contract”) or related to the proof methodology and tools used (like “the type system of the program should not be bypassed”). The problem is that the overall verification of a software, as done in certification, should ultimately discharge such assumptions, either by some other automatic verification activity, or by manual review. Because assumptions are not taken for granted in software certification.

Researchers have started taking assumptions seriously, in particular for certification. See for example this paper at FM 2012, and the paper “Tool Integration with the Evidential Tool Bus” (or ETB) from SRI. The Frama-C platform already has a built-in mechanism for storing the assumptions on which individual proofs of properties depend (see their paper “Combining Analyses for C Program Verification”). The SPARK technology also provides a way to summarize how all properties of interest were checked, inclusing manual review, so that there are no pending assumptions besides the implicit ones depending on the approach.

What we have been discussing last Monday with Simon Cruanes (a coauthor of the SRI paper above) and Frama-C team members Julien Signoles and Virgile Prevosto, is how to combine verification results from different tools (some doing formal verification, some doing dynamic verification like testing) on different languages (Ada and C) in a way that no assumption is forgotten. The Datalog language used to express constraints in the ETB seems a good start. We are now going to experiment with the ETB and its Datalog language to see if that allows us to express and check the verification constraints mandated by various certification standards, for our tools.

Note that the CEA will host soon Maria Christakis (a coauthor of the FM 2012 paper above) and SRI researchers Natarajan Shankar and Sam Owre, which whom we’ll discuss this topic. To be continued.

Posted in Certification | Tagged , , , | 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 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
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @