1 The Crazyflie weighs only 19 g and has a 72 MHz CortexM3 processor Another Cortex core is found on the wireless chip Image courtesy of Bitcraze

Ada/SPARK Fixes Crazyflie Nano Quadrotor

Aug. 25, 2015
Crazyflie quadrotor is an open-source project including the hardware. I tried out a project where the control software was rewritten in SPARK, a subset of Ada.

>> Website Resources
.. >> Library: TechXchange
.. .. >> TechXchange: Embedded Software
.. .. .. >> Topic: Ada and SPARK

I just got my hands on the Crazyflie quadrotor (Fig. 1) from Bitcraze. The aircraft is an open-source project including the open-source hardware. It is designed as a development platform, unlike most other quadrotors that tend to be closed systems. The software can be downloaded and a control application runs on a PC. It supports a Sony Dual Shock controller. 

I ran through the Crazyflie checklist and pulled out my Sony controller from my PS3. The system works nicely, but the reason I really got the Crazyflie was to check out Anthony Gracio’s SPARK project (see "How to prevent drone crashes using SPARK"). Anthony is an intern at AdaCore and he rewrote the control software in SPARK, a subset of Ada.

The control software and library is written in C++. That is not surprising given that C and C++ tend to be the languages used for most deeply embedded projects like this. They are also part of the typical toolset available from chip vendors like ST Microelectronics that build the Cortex-M3 chip used in the Crazyflie.

Anthony used Adacore’s standard tool chain that is available as an open-source project. SPARK is designed for high-integrity software and it provides a platform that is much better than most for employing static and dynamic verification. Adacore also has a SPARK Pro version available.

One new feature of Ada and SPARK is the concept of contracts (see “Ada 2012: The Joy of Contracts” on Electronic Design). It was part of Ada 2012 and formalized the implementation that originally started with SPARK using a preprocessor. It allows “contract-based programming.” This is where the procedures or methods are annotated with contracts that specify inputs and outputs. This is in addition to the range-checking already inherent in Ada.

Swapping out the C++ code for the SPARK code is a relatively trivial exercise. It is essentially the same as dropping in a new version of the C++ code. The difference is the quality. Anthony found and corrected a number of bugs due to the use of SPARK. Functionally the SPARK code is identical with the bug fixes.

I would really like to see the Crazyflie project switch over to SPARK, but I suspect that C++ aficionados are not taking the hint. In the meantime, I hope to get a chance to do some SPARK coding.

>> Website Resources
.. >> Library: TechXchange
.. .. >> TechXchange: Embedded Software
.. .. .. >> Topic: Ada and SPARK

About the Author

William G. Wong | Senior Content Director - Electronic Design and Microwaves & RF

I am Editor of Electronic Design focusing on embedded, software, and systems. As Senior Content Director, I also manage Microwaves & RF and I work with a great team of editors to provide engineers, programmers, developers and technical managers with interesting and useful articles and videos on a regular basis. Check out our free newsletters to see the latest content.

You can send press releases for new products for possible coverage on the website. I am also interested in receiving contributed articles for publishing on our website. Use our template and send to me along with a signed release form. 

Check out my blog, AltEmbedded on Electronic Design, as well as his latest articles on this site that are listed below. 

You can visit my social media via these links:

I earned a Bachelor of Electrical Engineering at the Georgia Institute of Technology and a Masters in Computer Science from Rutgers University. I still do a bit of programming using everything from C and C++ to Rust and Ada/SPARK. I do a bit of PHP programming for Drupal websites. I have posted a few Drupal modules.  

I still get a hand on software and electronic hardware. Some of this can be found on our Kit Close-Up video series. You can also see me on many of our TechXchange Talk videos. I am interested in a range of projects from robotics to artificial intelligence. 

Sponsored Recommendations

Comments

To join the conversation, and become an exclusive member of Electronic Design, create an account today!