Polyspace Code Prover

Integrierte Software in C und C++ verifizieren

Polyspace Code Prover führt Codeverifikationen für integrierte Software in C and C++ aus, die höchsten Qualitäts- und Sicherheitsstandards entsprechen muss. Es wird eine Technik der formalen Methoden verwendet, die sich abstrakte Interpretation nennt, um zuverlässige Verifikationsergebnisse zu erhalten. Polyspace Code Prover erkennt, wo Laufzeitfehler auftreten können, und Code, der erwiesenermaßen sicher vor Laufzeitfehlern ist. Sie verwenden Polyspace Code Prover als Teil eines anspruchsvollen Qualitätssicherungsprozesses zur gründlichen Verifikation aller Eingaben, Pfade und Variablenwerte. Polyspace Code Prover verwendet eine Farbkodierung, die den Status der einzelnen Elemente im Code anzeigt. Durch die Integration mit Simulink® bietet Polyspace Code Prover die Rückverfolgbarkeit von Laufzeitergebnissen auf Codeebene zu den Simulink-Modellen.

Polyspace Code Prover bietet folgende Möglichkeiten:

  • Bestätigung Ihres Codes: Es wird verifiziert, dass Ihr Code frei von Laufzeitfehlern ist.
  • Ergebnisse ohne falsch negative Ergebnisse: Gründliche Suche nach allen potentiellen Laufzeitfehlern.
  • Umsetzung einer zuverlässigen Codequalität: Gegenüberstellung von bewiesenem Code und unbewiesenem Code

Der Zugriff auf Polyspace Code Prover erfolgt über die Befehlszeile, eine grafische Benutzeroberfläche oder über Plug-Ins für Visual Studio® und Eclipse™. Sie verwenden das Programm zur Unterstützung aller kritischen Aktivitäten in einem Softwareentwicklungs-Workflow. Dazu gehören folgende:

  • das Erkennen von Laufzeitfehlern
  • das Bestätigen der Abwesenheit bestimmter Laufzeitfehler
  • das Bestimmen von Variablenbereichen und Sicherstellen, dass Bereichsgrenzen nicht überschritten werden
  • das Sicherstellen, dass die entsprechenden Softwarequalitätsziele erreicht werden
  • das Rückverfolgen von Laufzeitfehlern zu Simulink-Blöcken oder IBM® Rational® Rhapsody®-Modellen
  • das Erstellen von Zertifizierungsartefakten

Zusammen mit Polyspace Bug Finder sucht Polyspace Code Prover Fehler und prüft die Konformität mit Codierungsstandards. Diese Produkte bieten eine umfassende Funktion zur statischen Analyse, die frühzeitig im Entwicklungsprozess genutzt werden kann, um Fehler zu lokalisieren, Coderegeln zu prüfen und Nachweise für Laufzeitfehler zu liefern. Diese Funktion stellt die Zuverlässigkeit von integrierter Software sicher, die höchste Ansprüche an Qualität und Sicherheit erfüllen muss.

Sie können die Codeverifikation beschleunigen und auf einen Computer-Cluster auslagern, indem Sie Verifikationsjobs mit Parallel Computing Toolbox™ und dem MATLAB Distributed Computing Server™ übergeben.

Weiter: Laufzeitfehler erkennen

Probieren Sie Polyspace Code Prover

Testsoftware anfordern

Kein Spaß an Code Reviews? Automatische Verifikation!

Webinar anzeigen