Free booklet, co-authored by Thales, explains how to exploit SPARK/Ada technology to achieve high levels of software assurance
ANNAPOLIS, Md., High Confidence Software and Systems Conference, May 8, 2017 – AdaCore today announced the publication of a free booklet, Implementation Guidance for the Adoption of SPARK, which explains how best to introduce and make use of the SPARK/Ada formal verification technology based on a project’s assurance goals. Co-authored by AdaCore and Thales, a global technology leader in critical domains, the booklet describes the various levels of software assurance at which the SPARK language and toolset can be used. It explains the associated benefits and costs at each level, and details the processes that Thales is using to introduce formal verification in operational projects. The booklet will be a valuable resource for project leaders, technology experts, and software developers responsible for producing high-assurance software for critical systems.
After briefly introducing the Ada language and its SPARK subset, the booklet describes four levels of software assurance:
- Stone level – Adhering to the SPARK subset. This is an intermediate step during technology adoption.
- Bronze level – Proving proper initialization and correct data flow. This level is recommended for the largest part of the code that is possible and will, among other things, prevent reads of uninitialized variables and misuses of global data.
- Silver level – Proving absence of run-time errors. This level is recommended for critical software, for example if it needs to be certified against software standards such as DO-178B and DO-178C (avionics) or EN 50128 (rail).
- Gold level – Proving key integrity properties. This level is appropriate for a subset of code where critical safety or security properties need to be shown.
A fifth level, Platinum, entails a full functional proof that the software meets its formally specified requirements. This level is outside the scope of the booklet.
“From our years of providing SPARK solutions to critical industries, we know that it can take time and effort to introduce disruptive technologies into an established workflow, even when the benefits are clear,” said Yannick Moy, SPARK Product Manager at AdaCore. “That’s why I’m pleased that we had the opportunity to work with Thales on this booklet. Now any organization developing and verifying high-assurance software will find practical guidance on how to adopt and best exploit SPARK technology.”
“Introducing formal verification in a project requires an informed scoping of the targeted software functions, as well as a clear definition of the verification objectives,” said Véronique Normand, Research & Technology Manager at Thales. “This booklet is intended to help teams characterize their verification objectives, and to provide practical implementation guidance in applying SPARK. Developed together with several Thales software architects, it is now used to support further SPARK initiatives in the Thales Group.”
About AdaCore
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings:
- The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
- The SPARK Pro verification environment, a toolset based on formal methods and oriented toward high-assurance systems,
- The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software, and
- The QGen model-based development tool, a qualifiable and customizable code generator and verifier for Simulink® and Stateflow® models, intended for safety-critical control systems.
Over the years, customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as railway systems, space systems, commercial avionics, military systems, air traffic management/control, medical devices and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/customers/ for further information.
AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com
About Thales
Thales is a global technology leader for the Aerospace, Transport, Defense and Security markets. With 64,000 employees in 56 countries, Thales reported sales of €14.9 billion ($16 billion) in 2016. With over 25,000 engineers and researchers, Thales has a unique capability to design and deploy equipment, systems and services to meet the most complex security requirements. Its exceptional international footprint allows it to work closely with its customers all over the world.
Availability
The booklet is available for free, both on-line and as a paper copy; please visit http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/
or contact info@adacore.com.
