Polyspace Code Prover analysiert alle Codepfade aller möglichen Eingaben, um das Fehlen bestimmter Laufzeitfehler wie Überlauf, Division durch Null und Zugriff auf Arrays außerhalb der Grenzen in C/C++ Code zu beweisen. Es liefert außerdem Einblicke in die Steuerung und den Datenfluss und beweist die Korrektheit des gleichzeitigen Zugriffs auf globale Variablen, die von mehreren Tasks (Threads) gemeinsam genutzt werden.
Polyspace Code Prover verwendet statische Analyse durch abstrakte Interpretation auf Basis formaler Methoden und liefert Ergebnisse, ohne dass Programmausführung, Codeinstrumentierung oder Testfälle erforderlich sind. Die Ergebnisse sind leicht verständlich und umsetzbar: Sie erscheinen direkt im Quellcode mit farbcodierten Fundstellen, Informationen zum Variablenbereich und Codenavigation. Sie können Polyspace Code Prover für jede beliebige Kombination von C/C++ Code verwenden, egal ob dieser manuell geschrieben oder von Simulink oder einem KI-Assistenten generiert wurde.
Die Unterstützung von Branchenstandards ist möglich über das IEC Certification Kit (für IEC 61508 und ISO 26262) und das 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.
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 Copilot
Ein für Polyspace optimierter KI-Assistent.
Polyspace Test
Entwicklung, Verwaltung und Durchführung von Tests für C und C++ Code in Embedded Systems.
Polyspace as You Code
Erkennen Sie Software-Schwachstellen und Verstöße gegen Codierungsstandards über Ihre IDE.
Polyspace Test Server
Führen Sie Tests und Analysen der strukturellen Abdeckung von C/C++ Code auf Automatisierungsservern aus.
Polyspace Code Prover Server
Verifizieren Sie laufend und umfassend kritische Anweisungen in C und C++ Code in CI-Pipelines.
Polyspace Bug Finder
Überprüfen Sie Programmierregeln, Sicherheitsstandards und Codemetriken und finden Sie Bugs.
Polyspace Client for Ada
Erstellen Sie mithilfe formaler Methoden umfassende Verifikationen für Ada-Anweisungseinheiten.
Polyspace Bug Finder Server
Ermitteln Sie Softwarefehler und setzen Sie Programmierregeln in Ihren CI-Pipelines durch.
Polyspace Server for Ada
Erstellen Sie laufende und umfassende Verifikationen für kritische Ada-Codeanweisungen in CI-Pipelines.
Polyspace Code Prover
Erstellen Sie mithilfe formaler Methoden umfassende Verifikationen für besonders kritische C und C++ Anweisungen.
Polyspace Code Prover – Häufig gestellte Fragen
Polyspace Code Prover weist das Fehlen kritischer Laufzeitfehler wie Überläufe, Division durch Null und Array-Zugriffe außerhalb der Grenzen in C/C++-Code nach. Es bietet zudem architektonische Ansichten wie Aufrufgraphen und die Nutzung globaler Daten, um die Softwarestruktur aus dem Code heraus besser zu verstehen.
Polyspace Code Prover verwendet eine auf formalen Methoden basierende statische Analyse, um alle Ausführungspfade und Eingaben in C/C++-Code zu untersuchen, ohne diesen auszuführen.
Polyspace Code Prover zeigt die Ergebnisse direkt im Quellcode an, mithilfe farbcodierter Anmerkungen, die anzeigen, ob Operationen als frei von Laufzeitfehlern bewiesen, als fehlerhaft nachgewiesen, unerreichbar oder unbelegt sind. Es liefert außerdem Wertebereichsinformationen für Variablen und Funktionsrückgabewerte, um die Ursachenanalyse zu unterstützen.
Es verbessert die Softwaresicherheit, indem es das Fehlen kritischer Schwachstellen wie Buffer Overflows, ungültige Speicherzugriffe und numerische Überläufe über alle Ausführungspfade und Eingaben hinweg nachweist, ohne den Code auszuführen.
Polyspace Code Prover verwendet formale Methoden, um das Fehlen ausgewählter Laufzeitfehler erschöpfend zu beweisen. Polyspace Bug Finder erkennt Fehler, Verstöße gegen Programmierregeln und Metriken zur Codequalität in vollständigen Projekten während Integration und Verifikation. Polyspace as You Code führt eine Teilmenge der Analysen von Polyspace Bug Finder direkt in der IDE aus, um Entwickler beim Erkennen von Problemen während des Schreibens von Code zu unterstützen.
Polyspace Code Prover wird interaktiv in einer Desktop‑Benutzeroberfläche verwendet, während Polyspace Code Prover Server für automatisierte Analysen in CI-Workflows und das Teilen von Ergebnissen über Polyspace Access optimiert ist.
a, es kann automatisch generierten Code analysieren, wobei die Ergebnisse zurückverfolgbar zu Simulink‑Modellen und dSPACE TargetLink‑Blöcken sind. Wenn die Analyse aus Simulink ausgeführt wird, wird sie automatisch basierend auf dem Modell und den Codegenerierungseinstellungen konfiguriert.
Es unterstützt Zertifizierungs‑Workflows für IEC 61508, ISO 26262, EN 50128, EN 50657, IEC 62304, ISO 25119 und DO 178C/ED 12C durch Zertifizierungs‑ und Qualifizierungs‑Kits, mit zusätzlicher Anleitung für ISO/SAE 21434 und Automotive SPICE.
Interessiert an Polyspace Code Prover?
Nächste Schritte
Navigation im Panel
KOSTENLOSE ARTIKEL
Hinweise zu Polyspace
Navigation im Panel
PRODUKT
