>> Website Resources
.. >> Library: TechXchange
.. .. >> TechXchange: Embedded Software
.. .. .. >> Topic: Ada and SPARK
Download this article as a .PDF
Developing safe and secure systems can be a challenging task, but one can be made easier with the right tools. Many such tools, like static analysis, can be applied to languages like C and C++ that inherently lack this support, versus languages like SPARK and RUST that incorporate these techniques as part of their definition—making them available to all programmers who use the language.
SPARK, a subset of Ada 2012, goes the extra mile with provable static analysis, but utilizing all of its advantages can be daunting. Still, incremental use of these features can provide significant benefits, and using a subset of them may be suitable in many instances. This is similar to the MISRA support for C and C++ that are a collection of rules that can be selectively applied for many projects. MISRA C and other coding standards provide a way to improve the quality of the code created by programmers.
The white paper, "Implementation Guidance for the Adoption of SPARK," was developed by Adacore and Thales, two companies involved in high assurance systems. It presents a multilevel approach to using SPARK in high assurance development environments. The levels spelled out in the paper include:
- Stone – Valid SPARK code
- Bronze – Initialization and correct dataflow
- Silver – Absence of run-time errors
- Gold – Proof of key integrity properties
This isn’t the first system to utilize this type of naming convention. Intel’s latest processor line has gone down this road, as well.
Check out the paper for details, as the description and examples are more extensive that can be covered here. These examples are written in Ada/SPARK, for obvious reasons, but they can also be instructive to those using different platforms to highlight issues common to the creation of high-assurance applications.
There are many myths about Ada, and even less is known of SPARK by most embedded programmers where C and C++ dominate. Using good tools and coding standards can significantly decrease the number of bugs generated over the course of a development program without significantly increasing the amount of time taken to create applications. In fact, the time to develop a safe and secure application can actually be less that that needed to create the application using a less structured approach.
