Polyspace Code Prover

Nachweisen, dass die Software keine Laufzeitfehler enthält

Mit Polyspace Code Prover™ können Sie nachweisen, dass der C- und C++-Quellcode frei von Fehlern des Typs Überlauf, Division durch Null, unzulässiger Array-Zugriff und frei von bestimmten anderen Laufzeitfehlern ist. Ergebnisse werden geliefert, ohne dass eine Ausführung des Programms, eine Codeinstrumentierung oder Testfälle erforderlich sind. Polyspace Code Prover verwendet die statische Analyse und die abstrakte Interpretation auf der Basis von formalen Methoden. Daher können Sie handgeschriebene Codes, generierte Codes oder eine Kombination aus beiden verwenden. Jeder Vorgang ist farblich codiert, um anzuzeigen, ob er frei von Laufzeitfehlern ist, erwiesenermaßen fehlschlagen wird, nicht erreichbar oder unbewiesen ist.

Polyspace Code Prover zeigt auch Bereichsinformationen für Variablen und Funktionsrückgabewerte an und kann Bedingungen nachweisen, unter denen Variablen bestimmte Bereichsgrenzen überschreiten. Ergebnisse können auf einem Dashboard veröffentlicht werden, um Qualitätsmetriken zu verfolgen und die Konformität mit Softwarequalitätszielen sicherzustellen. Polyspace Code Prover kann in Build-Systeme zur automatischen Verifikation integriert werden.

Die Unterstützung für Industriestandards ist verfügbar über IEC Certification Kit (für IEC 61508 und ISO 26262) und DO Qualification Kit (für DO-178). Die Unterstützung für die Sprache Ada ist ebenfalls verfügbar.

Kein Spaß an Code Reviews? Automatische Verifikation!

Webinar anzeigen

Probieren Sie Polyspace Code Prover

Testsoftware anfordern