La société d’ingénierie et de conseil en technologies avancées Altran et l’éditeur d’outils logiciels pour applications critiques AdaCore annoncent le lancement de l'environnement de vérification et de développement intégré ...Spark Pro 14.0 qui, selon ses concepteurs, apporte une nouvelle technologie de preuve et de vérification de logiciels ainsi que des caractéristiques de langage supplémentaires via la prise en charge du langage Spark 2014. Issu en partie des travaux menés au sein du projet de recherche Hi-Lite, Spark Pro 14.0 propose donc une approche intégrée de l'ensemble du cycle de développement et de vérification d’un logiciel critique en regroupant les aspects liés à la spécification logicielle, au codage et aux phases de test unitaire et de vérification formelle. Cet environnement a notamment été pensé pour mettre en œuvre les technologies de compilation et de preuve les plus récentes afin de fournir une vérification avancée d'un sous-ensemble du langage Ada.

Spark Pro 14.0 est en fait la première gamme d’outils à prendre en charge la toute dernière version du langage de programmation Spark 2014, basée sur le langage Ada 2012. Spark 2014 utilise et étend en particulier l'approche de la programmation par contrat introduite dans Ada 2012, permettant ainsi aux développeurs de code critique Ada d'exprimer et de vérifier les propriétés essentielles qu'un programme doit respecter. La technologie présente également une interface utilisateur améliorée avec des alertes générées par les outils ; celles-ci sont affichées sous forme de messages associés au code afin de permettre aux utilisateurs de comprendre l’origine des erreurs.

Enfin, Spark Pro 14.0 est conforme aux normes de sécurité des logiciels critiques DO-178B/C (et le supplément DO-333 pour les méthodes formelles), Cenelec 50128, CEI 61508 et Defstan 00-56. Cet environnement génère notamment les éléments de preuve nécessaires à la constitution d'un dossier d'assurance et démontre la conformité à ces différentes normes.