En poursuivant votre navigation sur ce site, vous acceptez l’utilisation de cookies pour vous proposer des contenus et services adaptés à vos centres d’intérêts. En savoir plus et gérer ces paramètres. OK X
 
 

 

 

Nouveaux produits

Un ensemble d’outils de vérification formelle

Publication: Février 2016

Partagez sur
 
Qui permet de réduire la démarche de certification des systèmes critiques en matière de sureté et de sécurité...
 

AdaCore a annoncé hier la sortie de la toute dernière version de son environnement intégré SPARK Pro de vérification et de développement qui propose une technologie d’analyse statique sûre, fondée sur des principes mathématiques permettant de résoudre les problèmes de vérification des logiciels des systèmes à haute fiabilité. SPARK Pro 16 propose une extension du langage SPARK 2014 et prend désormais en charge le profil multitâche Ravenscar, en élargissant de ce fait les avantages des méthodes de vérification formelle à un sous-ensemble sûr de caractéristiques de programmation concurrente en Ada 2012. Une autre avancée de SPARK Pro 16 est de pouvoir générer des contre-exemples aux obligations de preuve qu’il est impossible de vérifier, en permettant ainsi aux développeurs de trouver plus facilement les défauts du code fonctionnel ou des contrats fournis. SPARK Pro 16 optimise aussi la gestion des opérations bit à bit (modulaires) et le moteur de vérification du produit comprend désormais le solveur SMT Z3.

La technologie SPARK Pro qui a été développée conjointement par AdaCore et son partenaire Altran peut démontrer les propriétés du programme SPARK qui vont de l’absence d’erreurs d’exécution (exceptions) jusqu’au respect des spécifications formelles définies. De ce fait, SPARK Pro permet de réduire le coût des vérifications logicielles et simplifie la tâche de certification des logiciels par rapport aux standards de sûreté ou de sécurité. La technologie est sûre ; c’est-à-dire qu’il n’y a pas de « faux négatifs » : si SPARK Pro indique qu’un programme ne présente pas un certain type d’erreur, alors il est impossible que cette erreur se produise. Il présente également un taux très faible de « faux positif », et l’utilisation de solveurs SMT permet de traiter les projets larges et complexes. Le langage et l’ensemble des outils SPARK peuvent être utilisés dès le début de nouveaux projets ou être introduits progressivement dans un projet existant, ce qui offre une approche de vérification « hybride » associant des méthodes formelles à des techniques traditionnelles de test.

« Grâce à cette nouvelle version des outils SPARK Pro, nous nous approchons de notre objectif : permettre aux ingénieurs logiciel de commencer à faire vraiment confiance à la vérification statique et aux preuves formelles sans être experts en logique mathématique » a déclaré Cyrille Comar, le Président d’AdaCore. « Non seulement la plupart des preuves nécessaires sont menées de façon totalement automatique, mais bien des restrictions de langage généralement associées à ces capacités de preuve ont été levées. C’est ce qui permet l’écriture facile et agréable des logiciels éprouvés ».

Suivez MtoM Mag sur le Web

 

Newsletter

Inscrivez-vous a la newsletter d'MtoM Mag pour recevoir, régulièrement, des nouvelles du site par courrier électronique.

Email: