Electronique Mag - Le journal de l'électronique.

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 :

1. Niveau Pierre : Adhésion au sous-ensemble SPARK. Il s’agit d’une étape intermédiaire pendant l’adoption de la technologie.

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

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

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

http://www.adacore.com/