How to Prevent Drone Crashes Using SPARK

by Yannick Moy in Dev Projects, Formal Verification – May 28, 2015

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. 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. In this post, Anthony presents the work he did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped him to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.

Continue reading here.

comments powered by Disqus