Nachweis der Abwesenheit von Laufzeitfehlern mit ‚Sound Static Analysis‘
Astrée ist ein ‚Sound Static Analyzer‘, der die Abwesenheit von Laufzeitfehlern und ‚Dataraces‘ nachweist.
Astrée überprüft auf Abwesenheit von Fehlern. Es meldet Fehler, die durch nicht spezifiziertes und undefiniertes Verhalten gemäß den C- und C++-Sprachstandards verursacht werden, sowie Fehler, die durch ungültiges gleichzeitiges Verhalten verursacht werden. Des Weiteren berechnet Astrée Programmeigenschaften, welche für die funktionale Sicherheit relevant sind.
Keine ‚false-positives‘ & ‚false-negatives‘
Weniger ‚false-negative‘ Ergebnisse bedeuten mehr Sicherheit, dass die Analyse keine Probleme übersehen hat. Weniger ‚false-positive‘ Ergebnisse bedeuten weniger Aufwand für die Bewertung und das Verwerfen einer falsch gemeldeten Regelverletzung (Alarm).
‚Sound‘ Daten- und Kontrollflusskopplung
Astrée berechnet Daten- und Kontrollflussberichte, die eine detaillierte Auflistung der Zugriffe auf globale und statische Variablen enthalten. Diese Auflistung ist sortiert nach Funktionen oder Variablen, sowie den Aufruf-Beziehungen (caller/callee) zwischen den Funktionen
Gemeldete Fehlerklassen
Gleitkommaberechnungen werden von Astrée präzise und sicher behandelt. Es berücksichtigt alle möglichen Rundungsfehler.
WIE ASTRÉE IN IHREN VERIFIKATIONSPROZESS PASST
TESTEN > Nutzen Sie Cantata für die automatisierte dynamsiche Ausführung der standardkonformen Software.
> Nutzen Sie Cantata Hybrid, um zertifizierte Cantata Testergebnisse aus bestehenden Google Tests zu generieren.
ANALYSIEREN > Nutzen Sie Astrée für den Nachweis der Abwesenheit von Laufzeitfehlern in der gesamten Anwendung.
NB: Astrée verwendet dasselbe Konfigurationsformat wie QA-MISRA, somit ist der Aufwand für eine spätere Anwendung in einem QA-MISRA Projekt gering.