Select Language

AdaCore Releases SPARK Pro 16

Formal verification toolset helps reduce certification effort for safety-critical and high-security systems

ERTS2 2016, Toulouse, France, January 27, 2016 - AdaCore today announced the latest release of its SPARK Pro integrated development and verification environment, bringing a sound and mathematics-based static analysis technology to the challenges of software verification for high-assurance systems. SPARK Pro 16 provides enhanced coverage of SPARK 2014 language features and now supports the Ravenscar tasking profile, thus extending the benefits of formal verification methods to a safe subset of Ada 2012 concurrent programming features. As another improvement SPARK Pro 16 can generate counterexamples to verification conditions that cannot be proved, thus making it easier for developers to find defects in the functional code or in the supplied contracts. SPARK Pro 16 also improves the handling of bitwise (modular) operations, and the product’s proof engine now includes the Z3 SMT solver.

The SPARK Pro technology, which has been jointly developed by AdaCore and its partner Altran, can prove SPARK program properties ranging from absence of run-time errors (exceptions) to compliance with a formally defined requirements specification. SPARK Pro thereby helps reduce the cost of software verification and simplifies the task of certifying the software against safety or security standards. The technology is sound; that is, there are no “false negatives”: if SPARK Pro reports that a program is free of a certain kind of error, then that error cannot occur. It also has a very low “false positive” rate, which is important in practice, and its efficient SMT solver technology scales up for usage in large projects. The SPARK language and toolset can be used from the outset on new projects or introduced incrementally into an existing project, allowing a “hybrid” verification approach that combines formal methods with traditional testing techniques.

“With this new version of the SPARK Pro toolset, we get one step closer to our goal: to make it easy for software engineers to start relying heavily on static verification and formal proofs without needing expertise in mathematical logic,” said Cyrille Comar, AdaCore President. “Not only are most of the needed proofs conducted completely automatically, but many language restrictions usually associated with such proof capabilities have been lifted. This makes the writing of proven software both efficient and pleasant”.

About SPARK Pro
SPARK Pro provides the foremost language, toolset, and design discipline for engineering high-assurance software. It combines the SPARK language and verification tools with AdaCore’s GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments.

The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness, including proofs of the absence of run-time errors, which can then be used to meet the requirements of safety and security certification schemes, such as DO-178B and DO-178C (airborne systems), EN 50128 (railway systems), and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C.

About SPARK 2014
SPARK 2014 is a formally analyzable programming language especially suited for developing ultra-low defect software in critical applications, for example where safety and/or security are key requirements. The SPARK language has a solid industrial track record with a 25+ year history of successful usage worldwide in a range of industrial applications including civil and military avionics, railway signaling, cryptography, and cross-domain solutions. SPARK 2014 is the next generation of this leading software technology, offering key benefits such as support for hybrid verification (combining formal methods with traditional testing), executable contracts, a larger Ada language subset (for example including generic units), and convergence with Ada 2012 syntax (making it easier to combine Ada and SPARK components). An on-line interactive course on SPARK 2014, part of the AdaCore University curriculum, is available at http://university.adacore.com/courses/spark-2014/.

Availability
SPARK Pro 16 is available now. For more information please contact info@adacore.com, and for a demo please visit www.adacore.com/sparkpro/demos

About AdaCore
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems. Four flagship products highlight the company’s offerings:

  • The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
  • The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software,
  • The SPARK Pro verification environment, a toolset based on formal methods and oriented towards high-assurance systems, and
  • The QGen model-based development tool, a qualifiable and customizable code generator and verifier for Simulink® and Stateflow® models, intended for safety-critical control systems.

Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, rail systems, medical devices, and financial services. AdaCore has an extensive and growing world-wide customer base; see www.adacore.com/customers/ for further information.

AdaCore products are open source and come with expert on-line support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts
Jamie Ayre
AdaCore
press@adacore.com
http://twitter.com/AdaCoreCompany

Jenna Beaucage
Rainier Communications (for AdaCore)
Tel: +1-508-475-0025 x124
jbeaucage@rainierco.com

AdaCore stellt neues Release von SPARK Pro vor

Paris, 27. Januar 2016 – AdaCore hat die neueste Version seiner integrierten Entwicklungs- und Verifikationsumgebung SPARK Pro vorgestellt. Damit wird die Software-Verifikation für besonders sicherheitskritische Systeme um eine fundierte und mathematisch basierte, statische Analyse-Technologie erweitert.

SPARK Pro 16 bietet eine verbesserte Abdeckung der Sprachfunktionen von SPARK 2014 und unterstützt nun auch das Ravenscar-Tasking-Profil; dadurch werden die Vorteile formaler Verifikationsmethoden auf ein sicheres Subset der nebenläufigen Programmierung von Ada 2012 erweitert. Als eine weitere Verbesserung in SPARK Pro 16 können für Verifikationsbedingungen Gegenbeispiele erzeugt werden, die nicht bewiesen werden konnten; damit ist es für Entwickler leichter, Defekte im Funktionscode oder in den mitgelieferten Contracts zu finden. SPARK Pro 16 verbessert auch die Handhabung von Bitwise (modularen) Operations; außerdem enthält die Proof Engine nun den Z3 SMT Solver.

Die SPARK-Pro-Technologie, die gemeinsam von AdaCore und seinem Partner Altran entwickelt wurde, kann Eigenschaften von SPARK-Programmen prüfen, die von der Abwesenheit von Laufzeitfehlern (Exceptions) bis zur Einhaltung einer formal definierten Anforderungsspezifikation reichen. SPARK Pro hilft dadurch die Kosten der Software-Verifikation zu reduzieren und vereinfacht die Zertifizierung der Software. Die Technologie ist korrekt; es gibt also keine "False Negatives": Wenn SPARK Pro feststellt, dass ein Programm frei von einer bestimmten Art von Fehlern ist, dann können diese Fehler nicht auftreten. Außerdem ist die "False Positive"-Rate sehr gering; die effiziente SMT-Solver-Technologie skaliert auch für den Einsatz in Großprojekten. SPARK-Sprache sowie -Toolset können von vornherein bei neuen Projekten verwendet oder schrittweise in ein bestehendes Projekt eingebracht werden, wobei ein "hybrider" Verifikationsansatz, die Kombination formaler Methoden mit traditionellen Testtechniken, zulässig ist.

"Mit dieser neuen Version des SPARK-Pro-Toolsets sind wir unserem Ziel einen Schritt näher gekommen: Software-Ingenieuren den Einstieg in statische Überprüfung und formale Beweise einfach zu machen, ohne dass sie dafür Know-how in mathematischer Logik benötigen", sagt Cyrille Comar, AdaCore-Präsident. "Nicht nur, dass die meisten der benötigten Beweise vollautomatisch durchgeführt werden, es sind auch viele Spracheinschränkungen, die normalerweise mit solchen Nachweisen verbunden sind, aufgehoben. Das macht das Schreiben von geprüfter Software effizient und bequem."

SPARK Pro 16 ist ab sofort verfügbar, weitere Informationen unter info@adacore.com; eine Demo ist erhältlich unter www.adacore.com/sparkpro/demos

Über SPARK Pro und SPARK 2014

SPARK Pro bietet führende Programmiersprache, Toolset und Design-Regularien für das Engineering von Hoch-Sicherheitssoftware. SPARK Pro verbindet die SPARK-Sprache und Verifikationswerkzeuge mit AdaCores GNAT Programming Studio (GPS) und mit der integrierten Entwicklungsumgebung GNATbench.

Das SPARK-Pro-Toolset bietet statische Überprüfung, die hinsichtlich ihrer Solidität, der niedrigen Fehler-Alarm-Rate, des Umfangs und der Effizienz konkurrenzlos ist. Das Toolset garantiert die Korrektheit sowie die Abwesenheit von Laufzeitfehlern und kann verwendet werden, um die Anforderungen von Sicherheitszertifizierungen wie zum Beispiel DO-178B und DO-178C (Bordsysteme), EN 50128 (Eisenbahnsysteme) und der Common Criteria zu erfüllen. SPARK Pro lässt sich insbesondere im Zusammenhang mit dem Anhang "Formal Methods" zu DO-178C verwenden.

SPARK 2014 ist eine formal analysierbare Programmiersprache vor allem für die Entwicklung von Software mit besonders geringer Fehlerrate für kritische Anwendungen, zum Beispiel wenn Sicherheit eine Schlüsselanforderung ist. Die SPARK-Sprache hat eine mehr als 25-jährige Erfolgsgeschichte in zahlreichen industriellen Anwendungen, in der zivilen und militärischen Luftfahrtelektronik, der Eisenbahnsignaltechnik, bei Kryptographie und domänenübergreifenden Lösungen.

Über AdaCore
AdaCore wurde 1994 gegründet und bietet Tools für Software-Entwicklung und Verifikation für kritische und sicherheitskritische Systeme. Zu den wichtigsten Produkten von AdaCore gehören die GNAT-Pro-Entwicklungsumgebung für Ada, das statische Analyse-Tool CodePeer, die Verifikationsumgebung SPARK Pro und das modellbasierte Entwicklungswerkzeug QGen. Zahlreiche Anwender haben die AdaCore-Produkte im Einsatz und unterhalten damit eine Vielzahl von kritischen Anwendungen in Bereichen wie Raumfahrtsysteme, kommerzielle Luftfahrt, militärische Systeme, im Flugverkehrsmanagement, bei Schienensystemen, bei Geräten der Medizintechnik und bei Finanzdienstleistungen. AdaCore verfügt über eine umfangreiche und wachsende weltweite Kundenbasis; nähere Informationen dazu unter www.adacore.com/customers

AdaCore-Produkte sind Open-Source und werden mit Online-Support durch die Entwickler zur Verfügung gestellt. Das Unternehmen hat seinen nordamerikanischen Hauptsitz in New York, der europäische Hauptsitz ist in Paris. Weitere Informationen unter www.adacore.com

Pressekontakte:
AdaCore 
Jamie Ayre 
press@AdaCore.com
www.AdaCore.com
http://twitter.com/AdaCoreCompany

PR-COM GmbH
Romana Redtenbacher
romana.redtenbacher@pr-com.de
www.pr-com.de
Tel. +49-89-59997-761

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