Projet : Certyflie

Certyflie

Informations

  • Nom : Leonardo Gracio
  • Prénom : Anthony
  • Email : anthony.gracio@gmail.com
  • Ecole / Etablissement : AdaCore
  • Catégorie : Enterprise

Description du projet

Le marché des drones civils est en croissance exponentielle depuis quelques années. Avec ce nouvel usage, de nouvelles problématiques surgissent, notamment en ce qui concerne la sûreté de ces engins. En réponse à ces problématiques, les autorités imposent des régimes de certification de plus en plus stricts autour des logiciels de drones, avec des contraintes de plus en plus fortes en ce qui concerne leur développement et leur vérification.

SPARK 2014 est à la fois un langage de programmation et un ensemble d’outils de vérification. Cette technologie est destinée à remplir les exigences demandées pendant le développement de logiciels hautement critiques, notamment en ce qui concerne la certification. L’intérêt de SPARK est de pouvoir prouver l’absence d’erreurs à l’exécution ainsi que la concordance entre le code et sa spécification. L’exactitude de ce code est prouvée à l’aide de méthodes formelles.

Appliqué aux drones, SPARK constitue une excellente solution pour faciliter le développement de logiciels sûrs.

Le Crazyflie est un petit drone de loisir créé par Bitcraze en 2013. Son firmware écrit en C et entièrement open-source a fait de lui une excellente cible pour prouver qu’il était possible d’utiliser SPARK pour développer un logiciel de drone, et ce sans connaissances approfondies concernant les méthodes formelles.

La facilité d’interfacer du code SPARK avec du code écrit dans un autre langage a permis de se focaliser sur la partie la plus critique d’un logiciel de drone : son système de stabilisation. La réécriture du système de stabilisation du Crazyflie en SPARK a permis de prouver formellement l’absence d’erreurs d’exécution sur le code réécrit, en découvrant au passage des vulnérabilités dans le firmware initial.

La deuxième phase du projet a consisté à réécrire tout le système de tâches concurrentes ainsi que les pilotes de périphérique du Crazyflie en SPARK, en espérant pouvoir prouver l’absence d’erreurs liées à la concurrence grâce à la prochaine version de SPARK, actuellement en développement.

Quelques liens pour en savoir plus:
le projet sous github – https://github.com/AnthonyLeonardoGracio/crazyflie-firmware
une description technique d’une partie du travail – http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark
la critique de Bill Wong d’Electronic Design – http://electronicdesign.com/dev-tools/adaspark-fixes-crazyflie-nano-quadrotor-0