Bitcraze Forums

Hello everyone,

I'm currently doing a 6 months internship at AdaCore, a company providing commercial software solutions for the Ada language.

The subject of this internship is to rewrite the Crazyflie firmware in SPARK, a subset of Ada which is used for high reliability software. SPARK allows to prove absence of runtime errors (overflows, reading of uninitialized variables ...) and specification compliance of your program by using functional contracts.

The ultimate goal of SPARK is to prove the correctness of your program without executing it by using static analysis and formal proofs. It is usually used for critical systems (avionics, aerospace..).

Furthermore, it is easy to interface Ada/SPARK code with C code, which allows me to implement some of the Crazyflie functionalities (stabilization algorithms etc.), let the others in C (drivers..), and use them in my SPARK code.

I've already rewritten all the C functions which are related with the stabilization system and I've found some bugs in the C code that could lead to overflows or unwanted side effects (some of them has been corrected in your latest commits ).

Here is the GitHub link for those who are interested:

https://github.com/AnthonyLeonardoGraci ... e-firmware

Enjoy!

Sounds really interesting and I'll be sure to follow your progress!

Hello Bitcraze community

I've done a blog post explaining all the work I've been doing on the Crazyflie firmware using SPARK on the AdaCore Blog.

For those who are interested, here is the link: http://blog.adacore.com/how-to-prevent- ... sing-spark

Enjoy

Great! We'll make sure to spread it as well!