Suche   Â
AdaCore stellt neues Release von SPARK Pro vor
ID: 1313593
(firmenpresse) - 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 (www.adacore.com/sparkpro) bietet eine verbesserte Abdeckung der Sprachfunktionen von SPARK 2014 (www.spark-2014.org) 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(at)adacore.com; eine Demo ist erhältlich unter www.adacore.com/sparkpro/demos
Diese Presseinformation kann auch unter www.pr-com.de/adacore abgerufen werden.
Ãœ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.
Unternehmensinformation / Kurzprofil:
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
AdaCore
Jamie Ayre
press(at)AdaCore.com
www.AdaCore.com
http://twitter.com/AdaCoreCompany
PR-COM GmbH
Romana Redtenbacher
romana.redtenbacher(at)pr-com.de
www.pr-com.de
Tel. +49-89-59997-761
  
  
  
Datum: 27.01.2016 - 12:36 Uhr
Sprache: Deutsch
News-ID 1313593
Anzahl Zeichen: 4349
Kontakt-Informationen:
Ansprechpartner: Romana Redtenbacher
Stadt:
Paris
Telefon: +49-89-59997-761
Kategorie:
Internet
Meldungsart: Produktankündigung
Versandart: Veröffentlichung
Freigabedatum: 27.01.2016
Diese Pressemitteilung wurde bisher 0 mal aufgerufen.
Die Pressemitteilung mit dem Titel:
"AdaCore stellt neues Release von SPARK Pro vor"
steht unter der journalistisch-redaktionellen Verantwortung von
AdaCore (Nachricht senden)
Beachten Sie bitte die weiteren Informationen zum Haftungsauschluß (gemäß TMG - TeleMedianGesetz) und dem Datenschutz (gemäß der DSGVO).