Select Language

New SPARK Adoption Guidance Published

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. 

Press Contacts
press-info@adacore.com
http://www.adacore.com
http://twitter.com/AdaCoreComp...

US:
Jessie Glockner
AdaCore Public Relations Representative
+1-646-532-2723

EU:
Emma Adby
AdaCore Marketing Operations Manager
+33 1 49 70 87 82

 

Publication du nouveau guide d’adoption de SPARK

Ce livret gratuit, rédigé en collaboration avec Thales, explique comment exploiter la technologie SPARK/Ada pour atteindre des niveaux élevés d’assurance logicielle

ANNAPOLIS, Maryland, Conférence High Confidence Software and Systems, le 8 mai 2017 - AdaCore annonce la publication d’un livret gratuit, le guide Implementation Guidance for the Adoption of SPARK, expliquant le meilleur moyen de prendre connaissance et utiliser la technologie de vérification formelle SPARK/Ada en se basent sur les objectifs d’assurance du projet. Rédigé par AdaCore en collaboration avec Thales, l’un des leaders mondiaux dans les domaines critiques, le livret décrit les différents niveaux d’assurance logicielle pour lesquels le langage et l’outil SPARK peuvent être utilisés. Il explique les avantages et les coûts associés à chaque niveau et détaille les procédés utilisés par Thales pour introduire les techniques de vérification formelle dans des projets opérationnels. Le livret constituera une ressource précieuse pour les responsables de projets, les responsables en technologie et les développeurs de logiciels en charge de produire des logiciels avec un niveau d’assurance élevée pour les systèmes critiques.

Après une brève introduction du langage Ada et de son sous-ensemble SPARK, le livret décrit quatre niveaux d’assurance logicielle:

  • Niveau Pierre – Adhésion au sous-ensemble SPARK. Il s’agit d’une étape intermédiaire pendant l’adoption de la technologie.
  • Niveau Bronze – Démontre une bonne initialisation et un flux de données correct. Ce niveau est recommandé pour la majeure partie possible du code et permettra, entre autres, d’éviter la lecture de variables non initialisées et l’utilisation erronée de données globales.
  • Niveau Argent – Démontre l’absence d’erreurs d’exécution. Ce niveau est recommandé pour les logiciels critiques, par exemple en cas de besoin de certification selon des normes logicielles telles que DO-178B et DO-178C (avionique) ou EN 50128 (ferroviaire).
  • Niveau Or – Démontre des propriétés d’intégrité clés. Ce niveau est adapté pour un sous-ensemble de  code pour lequel des propriétés en termes de sûreté ou sécurité doivent être démontrées.

 

Un cinquième niveau, le Niveau Platine, comporte un ensemble complet de preuves fonctionnelles démontrant que le logiciel répond à des exigences formellement spécifiées. Ce niveau n’est pas couvert par le livret.

“Nous savons, grâce à notre expérience de la mise en œuvre de solutions SPARK à destinations d’industries critiques, que l’introduction de technologies de rupture dans un flux bien établi peut être longue et fastidieuse, même lorsque les avantages en sont clairs,” a indiqué Yannick Moy, Responsable de Produit SPARK chez AdaCore. “C’est pourquoi je suis ravi que nous ayons l’opportunité de collaborer avec Thales sur l’édition de ce guide, grâce auquel une organisation développant et vérifiant des logiciels avec des niveaux d’assurance élevée aura la possibilité de trouver des conseils pratiques sur la façon d’adopter et d’exploiter au mieux la technologie SPARK.”

“L’introduction des techniques de vérification formelle dans un projet implique une définition claire du champ des fonctions logicielles ciblées ainsi que des objectifs de vérification.,” a commenté Véronique Normand, Responsable Recherche et Technologie chez Thales. “Ce guide a pour but d’aider les équipes à caractériser leurs objectifs de vérification et de fournir des conseils pratiques d’application de SPARK. Développé en collaboration avec plusieurs architectes logiciels de chez Thales, il est à présent utilisé pour supporter plus encore les projets faisant appel à SPARK au sein du Groupe Thales.”

Á propos d’AdaCore
Fondée en 1994, AdaCore conçoit et fournit des outils de développement et de vérification de logiciels destinés à des applications pour lesquelles la sûreté, la sécurité et la fiabilité sont des éléments critiques. Quatre produits phares composent l’offre de la société :

  • GNAT Pro, l’environnement de développement pour Ada, une boîte à outils complète pour concevoir, mettre en œuvre et gérer des applications requérant un niveau élevé de fiabilité et de maintenabilité,
  • L’outil d’analyse statique avancé CodePeer, un réviseur et validateur automatique de code Ada capable de détecter et d’éliminer les erreurs aussi bien au cours du développement que rétrospectivement sur des logiciels existants,
  • L’environnement de développement SPARK Pro, un ensemble d’outils basés sur des méthodes formelles et orientés systèmes à niveau d’assurance élevé, et
  • L’outil de développement basé sur les modèles QGen , un générateur et vérificateur de code qualifiable et personnalisable pour les modèles Simulink® and Stateflow® destiné aux systèmes de contrôle critiques.

L'utilisation des produits AdaCore connaît une croissance continue dans des applications critiques telles que les systèmes spatiaux, l’avionique commerciale, les systèmes militaires, le contrôle aérien, les systèmes ferroviaires, les appareils médicaux ou les services financiers. AdaCore jouit d’une base fournie de clients internationaux en croissance constante; visitez le site www.adacore.com/customers/ pour de plus amples informations.

Les produits AdaCore sont libres et accompagnés d’un support expert en ligne fourni par les développeurs eux-mêmes. La société possède un siège nord-américain basé à New York et un siège européen basé à Paris. www.adacore.com

Á propos de Thales
Thales es un leader mondial dans les domaines de l’aérospatiale, des transports, de la défense et de la sécurité. Fort de ses 64.000 employés implantés dans 56 pays, Thales a déclaré 14,9 milliards d’€ ($16 milliards de $) de chiffre d’affaires en 2016. Avec plus de 25.000 ingénieurs et chercheurs, Thales possède une capacité unique à concevoir et déployer des équipements, des systèmes et des services capables de répondre aux exigences les plus complexes en termes de sécurité. Son exceptionnelle empreinte internationale lui permet de travailler en proche collaboration avec ses clients à travers le monde.

Disponibilité
Le livret est disponible gratuitement, aussi bien en ligne qu’en version imprimée.  Merci de vous rendre sur le lien http://www.adacore.com/knowledge/technical-papers/implementation-guidance-spark/ ou de contacter info@adacore.com. 

Contacts presse
press-info@adacore.com
http://www.adacore.com
http://twitter.com/AdaCoreComp...

Etats Unis :
Jessie Glockner
Représentante des Relations Publiques AdaCore
+1-646-532-2723

Europe :
Emma Adby
Responsable des Opérations Marketing AdaCore
+33 1 49 70 87 82