AdaCore publie SPARK Pro 16

Un ensemble d’outils de vérification formelle qui permet de réduire la démarche de certification des systèmes critiques en matière de sureté et de sécurité

ERTS² 2016, Toulouse, France, 28 janvier 2016 – 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.

Découvrez les applications des outils AdaCore dans le cadre de la certification DO-178B et des logiciels militaires.

À propos de SPARK Pro
SPARK Pro apporte une rigueur de premier plan en matière de langage, d’outils et de conception pour la réalisation de logiciels de haute fiabilité. SPAsRK Pro associe le langage SPARK et les outils de vérification aux environnements de développement intégrés GNAT Programming Studio (GPS) et GNATbench d’AdaCore.

La gamme d’outils SPARK Pro offre une vérification statique inégalée en termes de robustesse, de faible taux de fausses alarmes, de profondeur d’analyse et d’efficacité. La gamme d’outils génère la preuve de justesse des programmes, notamment les preuves d’absence de levée d’exceptions, qui peuvent être utilisées pour respecter les normes de certification de sûreté et de sécurité telles que DO-178B et DO-178C (systèmes aéroportés), EN 50128 (systèmes ferroviaires) et les Critères Communs (Common Criteria). SPARK Pro est spécialement applicable dans le contexte du supplément Méthodes Formelles de la norme DO-178C.

À propos de SPARK 2014
SPARK 2014 est un langage de programmation analysable formel spécialement adapté au développement des logiciels à très faible niveaux de défauts dans les applications critiques, par exemple lorsque la sûreté et/ou la sécurité sont des conditions clés. Le langage SPARK a des antécédents  industriels  solides au cours d’une histoire de + de 25 ans d’utilisation réussie dans le monde entier dans un éventail d’applications industrielles, notamment l’avionique civile et militaire, la signalisation ferroviaire, la cryptographie et les solutions transversales. SPARK 2014 représente la nouvelle génération de cette technologie logicielle de pointe, en proposant des avantages clés comme une assistance pour la vérification hybride (qui associe les méthodes formelles aux tests traditionnels), les contrats exécutables, un sous-ensemble étendu du langage Ada (par exemple avec des unités génériques) et une convergence avec la syntaxe Ada 2012 (ce qui facilite l’association de composants Ada et SPARK). Un cours interactif en ligne sur SPARK 2014, qui fait partie du cursus de l’université AdaCore, est disponible à l’adresse http//:university.adacore.com/courses/spark-2014.

Disponibilité
SPARK Pro 16 est disponible maintenant. Pour en savoir davantage, contactez info@adacore.com, et pour une démo, consultez le site www.adacore.com/spark/demos.

À propos d’Adacore 
Fondée en 1994, la société AdaCore fournit des outils de développement et de vérification  des logiciels critiques, nécessitant de hauts niveaux de sécurité et/ou de sûreté.

Quatre produits phares sont au cœur des offres de la société :

• L’environnement de développement GNAT Pro pour Ada, un ensemble complet d’outils pour concevoir, déployer et gérer des applications qui exigent une haute fiabilité, notamment pendant la phase de maintenance.
• L’outil d’analyse statique avancé CodePeer, un outil d’analyse et  de validation automatique d’Ada susceptible de détecter et d’éliminer les erreurs tant au cours du développement que rétrospectivement sur les logiciels existants.
• L’environnement de vérification SPARK Pro, un ensemble d’outils basé sur des méthodes formelles pour les systèmes très critiques, et
• L’outil QGen pour le développement basé sur les modèles, un générateur et vérificateur de code qualifiable et personnalisable pour les modèles Simulink® et Stateflow ®, destiné aux systèmes de contrôle critiques.

Au fil des années, nos clients ont utilisé les produits d’AdaCore pour établir et entretenir un large éventail d’applications critiques dans des domaines comme les systèmes spatiaux, l’avionique commerciale, les systèmes militaires, la gestion et le contrôle du trafic aérien, les systèmes ferroviaires, les dispositifs médicaux et les services financiers. AdaCore dispose d’une importante base de clients en pleine expansion dans le monde entier ; consulter le site www.adacore.com/customers/ pour en savoir davantage.

Les produits d’AdaCore sont open source et sont fournis avec une assistance en ligne assurée par les développeurs experts eux-mêmes. Le siège de la société se trouve en Amérique du Nord, à New York et en Europe à Paris. www.adacore.com.

Contact pour la presse
Jamie Ayre
AdaCore
press@adacore.com
http://twitter.com/AdaCoreCompany

Jenna Beaucage
Rainier Communications (pour AdaCore)
Tél. +1-508-475-0025, poste 124
jbeaucage@rainierco.com