>> Website Resources
.. >> Library: TechXchange
.. .. >> TechXchange: Embedded Software
.. .. .. >> Topic: Ada and SPARK
Safe and secure software is built using good tools and good designs capable of delivering code that’s as free of bugs as possible. Ada and SPARK, which are programming languages designed to reduce the number of bugs, tend to get utilized in areas like avionics that demand high reliability and safety. Ada and SPARK are also ideal for embedded devices down to the microcontroller level, like an Arm Cortex-M, where efficient code is crucial.
Avionics applications also often take advantage of Ada and SPARK tools due to the importance of certification. However, tool costs drift to the high side, and certification of tools is one aspect of the development process. Backwards compatibility and long-term support are critical as well.
AdaCore’s GNAT Pro tool suite, which has been supporting Ada and SPARK, and can support C and C++ development, was created to deal with those cost issues. AdaCore recently revamped and partitioned the product line into four editions: GNAT Pro Assurance, GNAT Pro Enterprise, GNAT Pro Developer, and the free, open-source GNAT Pro Community.
Assurance and Enterprise
The Assurance and Enterprise editions target AdaCore’s existing customers that need long-term support for multiple versions, and access to continuous patched releases. The Assurance edition provides sustained branch support, allowing very specific support to be provided to a customer. It also offers certification services.
The Assurance and Enterprise versions support Ada 83, Ada 95, Ada 2005, as well as the latest version, Ada 2012, along with SPARK. C and C++ support is optional. The Developer edition supports C, Ada 2012, and SPARK.
Developer and Community
The new Developer edition targets new Ada and SPARK developers. Of course, developers looking to learn or experiment with Ada and SPARK can use the free Community edition, but the Developer edition makes sense for commercial development. Its pricing is on par with commercial C/C++ development suites. It provides direct support and access to the continuous patched releases. The community edition gets updated, but with a longer update cycle.
Development platforms include Linux, macOS, and Windows, which also serve as targets. Furthermore, the Enterprise and Assurance editions support Solaris and AIX. Cross-platform support for these includes Android, PowerPC Linux, iOS, Lynx178, PikeOS, and VxWorks. All editions support bare-metal Arm platforms as well as embedded Linux. And all but the Community edition support QNX. This is significant, since QNX is used in high-reliability and safety application areas such as automotive.
The tool suites have a range of tools, including the GNATbench and GNAT Programming Studio IDEs. Among other interesting features are the Ada Web Server (AWS), GNATtest and GNATemulator.
The SPARK Discovery tool is part of the package and is aimed at developers new to SPARK and formal methods. Ada 2012 added SPARK contracts, which are used to do static, formal verification of applications. This allows developers to prove that an application meets specifications. Certification of C and C++ programs is usually done through a process and testing, rather than using formal methods on the code.
For example, Pre and Post conditions are contracts that can be applied to functions as shown in this Ada 2012/SPARK snippet:
This essentially forces the Insert function to require that the Last variable be a valid index to Queue before and after it’s called. This can be checked by the compiler or via runtime checks. Using formal methods to check the entire program makes it possible to eliminate the checks.
Of course, using these types of formal methods requires additional work, but it tends to be needed in high-assurance applications. It can also be very useful in general embedded application development by reducing the number of errors in an application and reducing checking overhead.
Developers and applications needn’t utilize the full power of SPARK to get started. Thales and AdaCore put together the "Implementation Guidance for the Adoption of SPARK" guide that spells out multiple levels of sophistication in terms of using SPARK. It starts with Stone, which is essentially valid SPARK code, and continues through Gold, where contracts and proofs are utilized throughout. The SPARK Discovery tool can be used in conjunction with the guide.
There are fewer Ada and SPARK developers when compared to most popular embedded languages like C, C++, and Java. Nonetheless, learning Ada and SPARK is relatively straightforward. Many myths are associated with Ada, but even a novice can quickly learn to program using these tools.
Companies looking to develop safe, secure, bug-free code for their applications should consider the advantages of using Ada and SPARK. Getting started is now more economical.
