Electronicdesign 15317 Adopting Spark 3

Helpful Hints for Adopting SPARK

May 9, 2017
Adacore and Thales have created a white paper addressing the incremental utilization of SPARK’s provability for high assurance applications.

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

  1. Stone – Valid SPARK code
  2. Bronze – Initialization and correct dataflow
  3. Silver – Absence of run-time errors
  4. 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.

Sponsored Recommendations

What are the Important Considerations when Assessing Cobot Safety?

April 16, 2024
A review of the requirements of ISO/TS 15066 and how they fit in with ISO 10218-1 and 10218-2 a consideration the complexities of collaboration.

Wire & Cable Cutting Digi-Spool® Service

April 16, 2024
Explore DigiKey’s Digi-Spool® professional cutting service for efficient and precise wire and cable management. Custom-cut to your exact specifications for a variety of cable ...

DigiKey Factory Tomorrow Season 3: Sustainable Manufacturing

April 16, 2024
Industry 4.0 is helping manufacturers develop and integrate technologies such as AI, edge computing and connectivity for the factories of tomorrow. Learn more at DigiKey today...

Connectivity – The Backbone of Sustainable Automation

April 16, 2024
Advanced interfaces for signals, data, and electrical power are essential. They help save resources and costs when networking production equipment.


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