La société AdaCore, spécialiste des outils et du langage Ada, vient de publier un livret gratuit, intitulé Implementation Guidance for the Adoption of Spark, dont l’objet est de mieux connaître la technologie de vérification formelle Spark/Ada. ...Rédigé en collaboration avec Thales, l’un des leaders mondiaux dans le développement et la mise en oeuvre de systèmes 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 notamment les avantages et les coûts associés de son utilisation à 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. Ce livret d’une soixantaine de pages, écrit en anglais, constitue ainsi une ressource pour les responsables de projets, les responsables en technologie et les développeurs 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, l’ouvrage décrit quatre niveaux d’assurance logicielle.

Le niveau “Pierre” est une adhésion au sous-ensemble Spark. Il s’agit d’une étape intermédiaire pendant l’adoption de la technologie.

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

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

Le niveau “Or” démontre quant à lui 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 à destination 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, explique Yannick Moy, responsable de produits Spark chez AdaCore. C’est pourquoi l’opportunité de collaborer avec Thales sur l’édition de ce guide va permettre à une organisation qui développe et vérifie des logiciels avec des niveaux d’assurance élevée, 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, précise Véronique Normand, responsable recherche et technologie chez Thales. Ce guide, utilisé en interne au sein des équipes de développement de Thales, a surtout pour but d’aider les équipes à caractériser leurs objectifs de vérification et de fournir des conseils pratiques d’application de Spark. »

L'ouvrage est acessible et téléchargeable gratuitement ici.