SPARK Pro 16 mit besserer Abdeckung der Sprachfunktionen

Die für die auf Ada basierende Programmiersprache SPARK gedachte Entwicklungsumgebung kommt vor allem bei der Software-Verifikation für besonders sicherheitskritische Systeme zum Einsatz.

In Pocket speichern vorlesen Druckansicht
SPARK Pro 16 mit besserer Abdeckung der Sprachfunktionen
Lesezeit: 2 Min.
Von
  • Alexander Neumann

AdaCore hat die Version 16 der vor allem bei High-Assurance-Systemen verwendeten Entwicklungs- und Verifikationsumgebung SPARK Pro vorgestellt. SPARK ist eine auf Ada basierende Programmiersprache, die Programme automatisch auf Korrektheit überprüfen kann. In dem von AdaCore mit Altran gemeinsam entwickelten SPARK Pro finden sich unter anderem die Werkzeuge GNAT Programming Studio und GNATbench.

Im neuen Release wurde die Abdeckung der Sprachfunktionen von SPARK 2014 überarbeitet. Es unterstützt nun auch das Ravenscar-Tasking-Profil, wodurch anscheinend die Vorteile formaler Verifikationsmethoden auf ein sicheres Subset der nebenläufigen Programmierung von Ada 2012 erweitert werden. Als eine weitere Neuerung lassen sich für Verifikationsbedingungen Gegenbeispiele erzeugen, die nicht bewiesen werden konnten. Damit soll es für Entwickler leichter werden, Defekte im Funktionscode oder in den mitgelieferten Contracts zu finden. Das neue Release verbessert außerdem die Handhabung sogenannter Bitwise (modularen) Operations, und zusätzlich enthält die Proof Engine nun den Z3 SMT Solver (Satisfiability Modulo Theories).

Das SPARK-Pro-Toolset garantiert die Korrektheit sowie die Abwesenheit von Laufzeitfehlern und kann verwendet werden, um die Anforderungen von Sicherheitszertifizierungen wie DO-178B und DO-178C (Bordsysteme), EN 50128 (Eisenbahnsysteme) und der Common Criteria zu erfüllen. SPARK Pro lässt sich auch im Zusammenhang mit dem Anhang "Formal Methods" zu DO-178C verwenden. Sprache sowie Toolset lassen sich von vornherein bei neuen Projekten verwenden oder schrittweise in ein bestehendes Projekt einbringen, wobei ein "hybrider" Verifikationsansatz, die Kombination formaler Methoden mit traditionellen Testtechniken, zulässig ist. (ane)