1. The Crazyflie weighs only 19 g and has a 72 MHz Cortex-M3 processor. Another Cortex core is found on the wireless chip. (Image courtesy of Bitcraze).
1. The Crazyflie weighs only 19 g and has a 72 MHz Cortex-M3 processor. Another Cortex core is found on the wireless chip. (Image courtesy of Bitcraze).
1. The Crazyflie weighs only 19 g and has a 72 MHz Cortex-M3 processor. Another Cortex core is found on the wireless chip. (Image courtesy of Bitcraze).
1. The Crazyflie weighs only 19 g and has a 72 MHz Cortex-M3 processor. Another Cortex core is found on the wireless chip. (Image courtesy of Bitcraze).
1. The Crazyflie weighs only 19 g and has a 72 MHz Cortex-M3 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

Sponsored Recommendations

Article: Meeting the challenges of power conversion in e-bikes

March 18, 2024
Managing electrical noise in a compact and lightweight vehicle is a perpetual obstacle

Power modules provide high-efficiency conversion between 400V and 800V systems for electric vehicles

March 18, 2024
Porsche, Hyundai and GMC all are converting 400 – 800V today in very different ways. Learn more about how power modules stack up to these discrete designs.

Bidirectional power for EVs: The practical and creative opportunities using power modules

March 18, 2024
Bidirectional power modules enable vehicle-to-grid energy flow and other imaginative power opportunities. Learn more about Vicor power modules for EVs

Article: Tesla commits to 48V automotive electrics

March 18, 2024
48V is soon to be the new 12V according to Tesla. Size and weight reduction and enhanced power efficiency are a few of the benefits.

Comments

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