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: http://blog.adacore.com/how-to-prevent-drone-crashes-using-spark

This entry was posted in Open-DO News. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

6 Comments

  1. Posted January 9, 2019 at 10:22 | Permalink

    Great content useful for all the candidates of SPARK training who want to kick start these career in the SPARK training field.

  2. Posted May 27, 2020 at 08:04 | Permalink

    Great Stuff! Check Out My Blog for more related stuff

  3. Posted June 9, 2020 at 11:41 | Permalink

    The importance of data analytics in the digital era
    Data Science Course Training in Pune

  4. shital
    Posted October 31, 2020 at 11:42 | Permalink

    Awesome blog. I enjoyed reading your articles. This is truly a great read for me. I have bookmarked it and I am looking forward to reading new articles.

    Data Scientist Course in pune

  5. Posted January 10, 2021 at 17:18 | Permalink

    wow, great, I was wondering how to cure acne naturally. and found your site by google, learned a lot, now i’m a bit clear. I’ve bookmark your site and also add rss. keep us updated.
    best data science courses in hyderabad

  6. Posted April 1, 2021 at 11:33 | Permalink

    Thank you for sharing this post, I really enjoyed reading every single word.

    Our Data Science course in Hyderabad will also help in seeking the highest paid job as we assist individuals for career advancement and transformation. We carefully curate the course curriculum to ensure that the individual is taught the advanced concepts of data science. This helps them in solving any challenge that occurs. Along with that, we also make students work on real case studies and use-cases derived.

    For More info Please Visit Our Site or else feel free to Call/WhatsApp us on +91-8008891188 or mail at info@technologyforall.in

    data science course in hyderabad

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*
 
  • Categories

  • Open-DO Projects

  • Contact

    info @ open-do.org