Astrée
Werkzeug zur statischen Quellcode-Analyse:
Erkennung von Laufzeit- und Gleichzeitigkeitsfehlern
Fünf Gründe, sich für Astrée zu entscheiden
Astrée ist ein auf formalen Methoden basierendes High-End-Tool, das sicherstellt, dass die Anwendung keine Laufzeitfehler aufweist, wenn es keine Laufzeitfehler entdeckt.
Bisher gibt es nur zwei auf formalen Methoden basierende Werkzeuge auf dem Markt, die diese Garantie bieten können.
1. es funktioniert
Funktioniert für Anwendungen, die in der Sprache C geschrieben sind.
2. Erkennen Sie
- Gleichzeitigkeitsfehler im OSEK-Betriebssystem und ARINC 653-Profil.
- Fehler bei der Division durch Null.
- Array-Zugriffsfehler außerhalb des Bereichs.
- Falsche Zeigermanipulationen.
- Überläufe von Ganzzahl- und Fließkomma-Variablen.
- Rundungsfehler bei Fließkommaberechnungen.
- Zugänge zu nicht initialisierten Variablen.
- Problematischer gleichzeitiger Zugriff auf Variablen, die von mehreren Prozessen gemeinsam genutzt werden.
- Fehler bei der Inkonsistenz von Variablensperren.
3. Ermöglicht
- Ermöglicht die Diagnose von benutzerdefinierten Assertions, um zusätzliche Eigenschaften zur Laufzeit zu testen.
- Ermöglicht die Prüfung, welche Teile des Codes unter keinen Umständen ausführbar sind(Erkennung von totem Code).
4. Prüfen Sie
Prüfen Sie den Quellcode anhand der folgenden Software-Codierungsstandards:
- MISRA C (2004 und 2012, einschließlich Änderungsantrag 1)
- C99 Sprache (Anhang J von ISO/IEC 9899:1999)
- CWE (CCR-Genauigkeiten Exakt, CWE-abstrakter und CWE-spezifischer)
- SEI CERT C
- ISO/IEC TS 17961:2012
5. Darüber hinaus...
- Es verfügt über eine IDE und eine Befehlszeilenschnittstelle, die eine Stapelverarbeitung ermöglicht, um Regressionstests zu erleichtern.
- Es bietet Integrationen mit Jenkins, SCADE, TargetLink (dSPACE), SymtaVision und RT-Druid.
- Es verfügt über einZertifizierungspaket für DO-178, ISO 26262, EN-50128 und FDA.
