Category Archives: Open-DO News

How to prevent drone crashes using SPARK

I recently joined AdaCore as a Software Engineer intern. The subject of this internship is to rewrite a drone firmware written in C into SPARK.

Some of you may be drone addicts and already know the Crazyflie, a tiny drone whose first version has been released by Bitcraze company in 2013. But for all of those who don’t know anything about this project, or about drones in general, let’s do a brief presentation.

The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. These two particularities allow the owner to add new features in an easy way. Moreover, a wiki and a forum have been made for this purpose, making emerge a little but very enthusiastic Crazyflie community!

Now that we know a little more about the Crazyflie, let me do a brief presentation of SPARK and show you the advantages of using it for drone-related software.

Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone!

But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events.

SPARK is an Ada subset used for high reliability software. SPARK allows proving absence of runtime errors (overflows, reading of uninitialized variables…) and specification compliance of your program by using functional contracts.

The advantages of SPARK for drone-related software are obvious: by using SPARK, you can ensure that no runtime errors can occur when the drone is flying. Then, if the drone crashes, you can only blame the pilot!

After this little overview, let’s see how we can use SPARK on this kind of code.

See more at:

Posted in Open-DO News | Leave a comment

Project P Open Workshop

Project-P Open Workshop
Model-driven engineering and qualifiable code generator

Project P is a three-year research project funded within the French FUI 2011 funding framework. It sees the collaboration of major industrial partners (Airbus, Astrium, Continental, Rockwell Collins, Safran, Thales), SMEs (AdaCore, Altair, Scilab Enterprise, STI), service companies (ACG, Aboard Engineering, Atos Origins) and research centers (CNRS, ENPC, INRIA, ONERA).

With the project now drawing to an end comes the final presentation of all the work that has been produced over the past 3 years…

Continental France, Project P leader, and all the project partners are pleased to invite you to the presentation of the final results of Project P.

The event will take place on Tuesday 16th June 2015 from 1:30pm to 5:30pm at Pôle Systematic – Palaiseau, Amphitheatre building N°3 – Nano-Innov

To find out more about access, please click here:


1:45pm – 2:00pm: Welcome

2:00pm – 4:00pm : Presentations

    Introduction to Project-P (Continental)
    Development and qualification of a generic code generation framework (ACGs)
    QGen: a qualifiable code generator for Simulink/Stateflow models (AdaCore)
    Operational use of a code generator (Sagem and Thales Alenia Space)
    Overview of other generators used in the project (AdaCore)
    A code generator for UML models (ATOS Origin)
    A formal verification perspective (IRIT)

4:00pm – 5:30pm : Workshop Demonstrations

    Model Verification and Code Generation with QGen (AdaCore)
    Hardware code generation with GAUT (LabSticc)
    Software code generation for XCOS models (Scilab Enterprise)
    Code generation from NSP language and Scicos (Inria/Altair/ENPC)
    Multi-formalism (UML and Simulink) code generation (ATOS/AdaCore)
    Generated code interoperability and schedulability analysis with SynDEx (INRIA)
    Verification of formal requirements for generated code (IRIT, ONERA)
    Description of formal requirements for generated code  (IRIT)

Registration is mandatory and closes on June 10th 2015 …to do so, please contact

Philippe CUENOT
Continental Automotive France
Tel : 05-61-19-88-88

Posted in Open-DO News | Leave a comment

SPARK Formal

The SPARK Formal project aims to develop a complete set of semantics of the SPARK language in Coq, for:

    - at the language level, ensuring the absence of ambiguity and the completeness of evaluation rules
    - at the tool level, ensuring the correct insertion of checks in the AST used for compilation and analysis

The formalization of SPARK also paves the way for the creation of proved toolchains for SPARK programs (a.k.a. “certified” toolchains in academia) such as CompCert.

Posted in Open-DO News | Leave a comment

Sparkel Programming Language

Sparkel is a new parallel programming language inspired by the SPARK subset of Ada, and designed to support the development of inherently safe and secure, highly parallel applications that can be mapped to multicore, manycore, heterogeneous, or distributed architectures.

To learn more about Sparkel and to follow the project, please visit
Posted in Open-DO News | Leave a comment

Ada for the C++ or Java Developer

This document will present the Ada language using terminology and examples that are familiar to developers that understand the C++ or Java languages.

To download the booklet, please visit this page

Posted in Open-DO News | 2 Comments

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 | 4 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

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
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @