La société AdaCore, éditeur d’outils de développement et de vérification de logiciels critiques qui nécessitent de hauts niveaux de sécurité et/ou de sûreté, a profité de l’événement ERTS 2016, qui s’est déroulé à Toulouse fin janvier, ...pour lancer la version 16 de son environnement de vérification Spark Pro qui propose une technologie d’analyse statique basée sur des méthodes d’analyse formelle. Spark Pro 16, qui associe le langage Spark et les outils de vérification GNAT Programming Studio et GNATbench d’Adacore, offre une extension du langage Spark 2014, un langage de programmation conçu pour être analysé formellement avec des outils mathématiques, et prend désormais en charge le profil multitâche Ravenscar, un sous-ensemble du langage Ada dédié aux systèmes temps réel nécessitant une sûreté de fonctionnement très élevée.
Autre caractéristique de cette version 16, la possibilité pour les programmeurs de générer des contre-exemples aux obligations de preuves qu’il est impossible de vérifier, afin de détecter plus aisément les défauts du code fonctionnel. Enfin, Spark Pro 16 optimise la gestion des opérations bit à bit et intègre le solveur SMT Z3, pour le traitement des projets larges et complexes.
Rappelons que la technologie Spark Pro, développée conjointement par Adacore et la société d’ingénierie Altran, génère des preuves de justesse d’un programme, et notamment les preuves d’absence de levées d’exceptions, utilisées en particulier pour respecter les normes de certification DO-178, DO-178C (aéronautique), EN 50128 (systèmes ferroviaires) et les Critères communs (Common Criteria). L’objectif affiché de Spark Pro est d’essayer de réduire les coûts de vérification des logiciels en simplifiant les tâches de vérification de ces derniers par rapport aux normes susnommées. Cet outil est utilisable dès le début d’un projet ou bien peut être mis en œuvre au cours d’un projet déjà existant, ouvrant alors la voie à une approche de vérification hybride associant méthodes de test classiques et méthodes formelles.
« Avec cette version de Spark Pro, nous approchons de notre objectif qui est de permettre aux ingénieurs logiciels de faire réellement confiance aux technologies de vérification statique et aux preuves formelles, sans qu'ils soient des experts en logique mathématique, explique Cyrille Comar, président d’AdaCore. Non seulement la plupart des preuves nécessaires sont menées de façon totalement automatique dans cet outil, mais, également, bien des restrictions de langage mathématique associées à ces capacités de preuves ont été levées. Ce qui permet une écriture plus facile de logiciels dûment éprouvés. »
