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.