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).
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.
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.
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.
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.
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.
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.
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.
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:
Polyspace-Produktfamilie
Polyspace-Produkte machen kritischen Code sicher und geschützt, indem die Softwarequalität während des gesamten Entwicklungslebenszyklus getestet und überwacht wird.
Polyspace Access
Erkennen Sie Codierfehler, überprüfen Sie die Ergebnisse statischer Analysen und überwachen Sie Softwarequalitätsmetriken.
Polyspace Code Prover Server
Nachweis der Abwesenheit von Laufzeitfehlern in Software.
Polyspace Bug Finder
Identifizieren Sie Softwarefehler mittels statischer Analyse.
Polyspace Test
Entwicklung, Verwaltung und Durchführung von Tests für C und C++ Code in Embedded Systems.
Polyspace Bug Finder Server
Erkennung von Softwarefehlern mithilfe statischer Analysen auf Servercomputern.
Polyspace Client for Ada
Nachweis der Abwesenheit von Laufzeitfehlern im Quellcode.
Polyspace Code Prover
Nachweis der Abwesenheit von Laufzeitfehlern in Software.
Polyspace Server for Ada
Code auf Computer-Clustern verifizieren und Metriken veröffentlichen.
Interessiert an Polyspace Code Prover?
Haben Sie Fragen?
Wenden Sie sich an das technische Team für Polyspace Code Prover.
