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

Near- and Far-Field Measurements

April 16, 2024
In this comprehensive application note, we delve into the methods of measuring the transmission (or reception) pattern, a key determinant of antenna gain, using a vector network...

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.

Empowered by Cutting-Edge Automation Technology: The Sustainable Journey

April 16, 2024
Advanced automation is key to efficient production and is a powerful tool for optimizing infrastructure and processes in terms of sustainability.


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