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

Interesting new UK conference

HIS 2014 is announced as “the UK conference for sharing information about the key challenges and recent developments in high integrity software engineering. This one day conference will be held in Bristol, UK on 23rd October 2014 and will feature presentations on current industrial experience as well as keynote talks from leading industry experts.”

An interesting program includes keynotes from Martyn Thomas and Harold Thimbleby and a number of international speakers. The talks are grouped into four main sessions:

    - Software Security
    - Software Safety
    - Applications
    - Languages and Technologies

More info and registration.

Posted in Certification, Events | Leave a comment

Parallel Programming Languages Enable Safer Systems

Languages that use garbage collection pose tricky issues for military system developers. In this recent article COTS journal article, Tucker Taft looks at innovative new parallel programming techniques that offer a safer solution.
Posted in Certification | Leave a comment

ERTS 2014: Integrated and Simpler Systems

I attended last week the 7th edition of the congress on Embedded Real Time Software and Systems that takes place in Toulouse (France) every two years. It started with Joseph Sifakis inviting all of us to work on the integration of embedded systems with Internet, and the Engineering Executive Vice-President of Airbus, Charles Champion, describing the many future challenges of avionics and asking, maybe surprisingly, for simpler software and systems to meet these challenges.

At the software level, I see two important trends contributing to these goals: model-based development and formal methods. The former because it facilitates communication between systems and software engineers, at the right level of abstraction, the latter because it makes the verification of these ever larger and integrated systems tractable thanks to abstraction and automation. No surprise then that both were very much present in presentations at the conference. A difference with previous years was that many of these presentations were backed by large industrial case studies. For example, for model-based development, the use of MBD in the context of DO-178C at Airbus Military, and for formal methods, the use of Event-B for requirements verification at BAE Submarine. The most interesting trend for me was the combination of model-based development and formal methods to manage greater integration between systems. We described such a workflow in our paper on System to Software Integrity. I expect more of these in the next edition.

Another highlight of this conference for me was certification, with two sessions dedicated to New Trends in Certification, among which a majority of papers on formal methods (5 papers). It will be interesting in the years to come to follow progress on the convergence of certification domains on the issues of tool qualification and formal methods.

Posted in Certification, Events | Leave a comment

Software Glitches: Why We Shouldn’t Put Up With Them

Robert Dewar discusses why software glitches are unacceptable in this day and age.

Software Glitches: Why We Shouldn’t Put Up With Them
Posted in In the Press | 2 Comments

Muen Separation Kernel

The Institute for Internet Technologies and Applications at the University of Applied Science in Rapperswil (Switzerland) and AdaCore today announced a significant expansion of the Open Source software model into the domain of high-assurance systems with the preview release of the Muen Separation Kernel. The Muen Kernel enforces a strict and robust isolation of components to shield security-critical functions from vulnerable software running on the same physical system. To achieve the necessary level of trustworthiness, the Muen team used the SPARK language and toolset to formally prove the absence of run-time errors.

More info.
Posted in Open Source, Related Initiatives | Leave a comment

Trusted Key Manager for IKEv2

The HSR University of Applied Sciences in Switzerland has implemented the TKM from scratch using the Ada programming language. The new Design-by-Contract feature of Ada 2012 has been used for the implementation of state machines, to augment the confidence of operation according to the specification. The TKM works in conjunction with the strongSwan IKEv2 daemon to provide key management services for IPsec.

Read the project report
Visit the TKM project page
Visit the strongSwan project page
Posted in Open Source | 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
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @