Die AbsInt-Toolchain für sicherheitskritische Systeme

Astrée – statische Laufzeitfehleranalyse

Überprüfen Sie Ihren C-Code auf Laufzeitfehler mit Astrée.

Finden Sie alle un­gültigen Zeiger­zugriffe, Divisionen durch Null, arithme­tische Über­läufe und Feld­grenzen­verletzungen. Entdecken Sie kritische Wett­läufe und andere Arten von Fehlern.

RuleChecker — automatische Überprüfung von MISRA-Regeln

Weisen Sie mit RuleChecker die Einhaltung von MISRA-Regeln nach.

Überprüfen Sie Ihren C-Code schnell und automatisch auf die Einhaltung von Standards wie MISRA, ISO/IEC, SEI CERT und CWE. Stellen Sie bei Bedarf Ihre ganz eigenen Zusatz­regeln auf. Überwachen Sie Code-Metriken wie Comment­dichte und zyklomatische Komplexität und erzeugen Sie Analyse­berichte zu Dokumentations- und Zertifizierungs­zwecken.

CompCert – verifiziertes Kompilieren

Kompilieren Sie den Code mit CompCert.

Erfüllen Sie die höchsten Sicher­heits­standards, indem Sie Ihre Anwendung mit dem einzigen Compiler übersetzen, der formal mathematisch verifiziert wurde. Damit gelten alle Sicherheits­eigenschaften, die Sie auf der Quellcode-Ebene nachgewiesen haben (z. B. mit Astrée), garantiert auch für den erzeugten Binärcode.

StackAnalyzer — statische Stackverbrauchsanalyse

Analysieren Sie den Stackverbrauch mit StackAnalyzer.

Be­rechnen Sie automatisch und exakt den maxi­malen Stack­ver­brauch Ihrer Anwendung für jeden Programm­punkt. Finden Sie alle Stack­überläufe, oder weisen Sie formal deren Abwesen­heit nach. Identifi­zieren Sie kritische Programm­teile und Ausführungs­pfade, und sparen Sie Zeit bei der Optimierung.

Analysieren Sie die Ausführungszeit mit aiT, TimingProfiler oder TimeWeaver.

aiT – statische WCET-Analysen

aiT

Berechnen Sie die schlimmstmögliche Ausführungszeit von Tasks in Ihren Binärdateien, ganz ohne aufwendige Tests und wiederholte Messungen. Die Analyse­ergeb­nisse gel­ten für alle Eingaben, alle mög­lichen Ausführungs­szenarien, alle Cache- und Pipeline-Zustände.

TimingProfiler — Timinganalyse in frühen Entwicklungsphasen

TimingProfiler

Wenn Ihre Anwendung noch früh in der Entwicklung ist und Sie sich für kein bestimmtes Prozessor-Derivat entschieden haben, hilft Ihnen TimingProfiler bei der Abschätzung der Ausführungs­zeit für eine ganze Prozessor­familie. Damit können Sie das Timing-Verhalten bereits ganz früh im Ent­wicklungs­prozeß überwachen, wenn Messungen an der Hard­ware zu kostspielig oder schlicht unmöglich sind.

TimeWeaver — hybrid WCET analysis based on execution traces

TimeWeaver

Profitieren Sie von statischen Analysen selbst für Prozessoren, die nur schwer zu modellieren sind, indem Sie statische Pfadanalysen mit Zeitmessungen aus dem Echtzeit-Tracing auf der Instruktionsebene verbinden.

Sonstige Produkte

Bei Fragen zu älteren oder kunden­spezifischen Pro­dukten wenden Sie sich an info@absint.com.