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