Polyspace Code Prover

Nachweis der Abwesenheit von Laufzeitfehlern in Software

Polyspace Code Prover weist die Abwesenheit von Überläufen, von Division durch Null, von Array-Zugriffen außerhalb der Bereichsgrenzen und von bestimmten weiteren Laufzeitfehlern in C und C++ Quellcode nach. Diese Ergebnisse erfordern weder eine Programmausführung noch eine Code-Instrumentierung oder Testfälle. Polyspace Code Prover arbeitet mit statischen Analysen und abstrakter Interpretation auf der Basis von formalen Methoden. Er lässt sich für handgeschriebenen und generierten Code sowie eine Mischung aus beidem verwenden. Jede Operation ist farblich markiert, um zu verdeutlichen, ob sie frei von Laufzeitfehlern ist, erwiesenermaßen fehlschlagen wird, nicht erreichbar oder unbewiesen ist.

Außerdem zeigt Polyspace Code Prover Bereichsinformationen für Variablen und für Ausgabewerte von Funktionen an und prüft, welche Variablen festgelegte Bereichsgrenzen überschreiten. Die Ergebnisse können auf einem Dashboard dargestellt werden, um Qualitätsmetriken mitzuverfolgen und die Einhaltung von Softwarequalitätszielen sicherzustellen.

Die Unterstützung von Branchenstandards ist möglich über das IEC Certification Kit (für IEC 61508 und ISO 26262) und DO Qualification Kit (für DO-178).

Verwendung von Polyspace Code Prover-Ergebnissen und Quellcodefarben.

Nachweis der Abwesenheit kritischer Laufzeitfehler

Analysieren Sie alle Codepfade auf potenzielle Eingaben ohne Codeausführung. Identifizieren Sie Anweisungen, die unabhängig von den Laufzeitbedingungen nie Laufzeitfehlern unterliegen, und finden Sie andere Fehler, die einen Eingriff erfordern.

Dokumentation

Anzeige eines Tooltipps mit möglichen Wertebereichen für Laufzeitbedingungen.

Besseres Software-Design und besseres Codeverständnis

Untersuchen Sie den Steuer- und Datenfluss in Ihrem C/C++ Code und zeigen Sie Wertebereichsinformationen zu Variablen und Operatoren an.

Dokumentation

Erkennen Sie toten Code in der Logik und der Programmstruktur.

Optimierung der Softwareleistung

Identifizieren Sie sichere Vorgänge und entfernen Sie defensiven Code wie die Division durch Null und Überlauf. Erkennen Sie Codezweige, die von keinem Ausführungspfad erreicht werden können. Finden Sie Fehler in der Logik und der Programmstruktur, die Sie entfernen können, um die Speicherbelegung zu verringern.

Dokumentation

Analyse der Verwendung globaler Variablen

Beschleunigen Sie das Debugging von Lese-/Schreibvorgängen mit globalen Variablen, einschließlich Variablen, die von Tasks oder Threads gemeinsam genutzt werden.
Verwenden Sie den Mehrfachzugriffs-Graphen, um Steuer- und Datenflüsse zu verstehen, die zu Data-Race-Problemen führen können. Identifizieren Sie ungenutzte globale Variablen für die Codeoptimierung.

Dokumentation

Zertifizierungsunterstützung

Erstellen Sie Artefakte, die für den Abschluss des Zertifizierungsvorgangs für Industriestandards erforderlich sind. Vom TÜV SÜD abgeschlossene Zertifizierung zur Verwendung mit den Normen IEC 61508 und ISO 26262. Verwenden Sie Berichte und Artefakte für DO-178C-Vorgänge.

Dokumentation

Integration von Simulink und Stateflow

Analysieren Sie generierten Code und verfolgen Sie Ihre Ergebnisse zu Simulink Modellblockquellen und Stateflow Diagrammen nach. Starten Sie eine Polyspace^® Analyse aus der Simulink-Umgebung.

Dokumentation

Interaktive Analysen auf Desktop-Computern.

Führen Sie statische Codeanalysen auf dem gesamten Softwareprojekt oder auf Teilen davon aus. Generieren Sie Berichte mit dem Desktop-Tool, um Ergebnisse zu überprüfen und vorzusortieren.
Ermitteln Sie die Ursache komplexer Programmierfehler mithilfe Debugger-ähnlicher Ansichten, um Schritt für Schritt durch jede Anweisung zu navigieren, die zu einem Laufzeitfehler führt. Organisieren und konfigurieren Sie Ihre Projekte mit der nativen Unterstützung von mehr als 60 C und C++ Compilern sowie der automatischen Einrichtung von aus dem Build-System des Projekts extrahierten Polyspace-Analysen.

Dokumentation

Statische Applikationssicherheitstests

Weisen Sie die Abwesenheit kritischer Sicherheitsschwachstellen wie Pufferüberläufen, Speicherzugriff und numerischen Überläufen nach. Verringern Sie den Fuzzing-Bedarf durch Codeanalyse für alle Codepfade und Eingaben ohne Codeausführung.

Auswirkungsanalyse

Verfolgen und verifizieren Sie formal die Auswirkungen einer festgelegten globalen oder lokalen Variable auf andere Variablen oder spezifische Anweisungen. Führen Sie Signalanalysen durch, um die Anforderungen des CARB für OBD-bezogene Software zu erfüllen, die Störungsfreiheit im Sinne von ISO 26262 nachzuweisen und die Auswirkungen von Kalibrierungsparametern zu analysieren. Führen Sie im Zusammenhang mit der Softwaresicherheit Taint-Analysen und eine Nachverfolgung des Flusses vertraulicher Daten durch.

Produktressourcen:

Dokumentation Beispiele Videos Technische Artikel Anforderungen Versionshinweise

Polyspace-Produktfamilie

Polyspace-Produkte machen kritischen Code sicher und geschützt, indem die Softwarequalität während des gesamten Entwicklungslebenszyklus getestet und überwacht wird.