>> 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