Polyspace Code Prover

Hauptmerkmale

  • Nachgewiesene Abwesenheit von bestimmten Laufzeitfehlern in C- und C++-Code
  • Farbcodierung von Laufzeitfehlern direkt im Code
  • Berechnung von Bereichsinformationen für Variablen und Funktionsrückgabewerte
  • Erkennung von Variablen, die vorgegebene Bereichsgrenzen überschreiten
  • Qualitätsmetriken zur Verfolgung der Konformität mit Softwarequalitätszielen
  • Anzeige von Codemetriken und Qualitätsstatus über ein webbasiertes Dashboard
  • Begleitetes Prüfverfahren zur Klassifizierung von Ergebnissen und Laufzeitfehlerstatus
  • Grafische Anzeige variabler Lese- und Schreibvorgänge
Run-time error results displayed by Polyspace Code Prover.

Von Polyspace Code Prover angezeigte Ergebnisse für Laufzeitfehler.

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.

Laufzeitfehler erkennen

Polyspace Code Prover verwendet abstrakte Interpretation mit statischer Codeanalyse, um Laufzeitfehler wie Überläufe, Division durch Null, Zeiger, die außerhalb des gültigen Bereichs liegen, nachzuweisen, zu identifizieren und zu diagnostizieren. Mit dieser Technik werden alle Laufzeitbedingungen vollständig und umfassend verifiziert. Für jede Codeoperation erfolgt die automatische Ausgabe der Diagnose „bewiesen“, „fehlgeschlagen“, „unerreichbar“, „unbewiesen“. In den von Polyspace Code Prover gelieferten Verifikationsergebnissen ist jede C- oder C++-Operation farbkodiert, um den entsprechenden Status anzugeben:

Grün: bewiesen „frei“ von Laufzeitfehlern
Rot: bewiesen „fehlerhaft“ bei jedem Ausführen der Operation
Grau: bewiesen „unerreichbar“ (möglicherweise ein funktionales Problem)
Orange: „unbewiesene“ Operation ist möglicherweise unter bestimmten Bedingungen fehlerhaft

Color-coded run-time error attributes identified by Polyspace Code Prover.

Von Polyspace Code Prover identifizierte Attribute für Laufzeitfehler.

Folgende Fehler werden erkannt:

  • Überlauf, Unterlauf, Division durch Null und andere arithmetische Fehler
  • unzulässiger Array-Zugriff und unerlaubt dereferenzierte Zeiger
  • immer wahr/falsch-Anweisung
  • nicht-initialisierte Klassenmember (C++)
  • Lesezugriff auf nicht initialisierte Daten
  • Zugriff, um diesen Zeiger (C++) für ungültig zu erklären
  • toter Code
  • dynamische Fehler in Bezug auf Objektprogrammierung, Vererbung und Ausnahmebehandlung (C++)

Bereichsinformationen anzeigen

Polyspace Code Prover verfolgt den Steuerungs- und Datenfluss durch die Software und zeigt Bereichsinformationen an, die im Zusammenhang mit Variablen und Operatoren stehen. Wenn Sie den Cursor über einem Operator oder einer Variablen positionieren, wird ein Tooltip mit den Bereichsinformationen angezeigt. Die formale Methode, die als abstrakte Interpretation bezeichnet wird, ermöglicht die Bestimmung präziser Bereichsinformationen, anhand derer nachgewiesen wird, dass die Software frei von bestimmten Laufzeitfehlern ist. Sie können Bereichsinformationen verwenden, um Ihre Software zu debuggen oder um sicherzustellen, dass bestimmte Variablen oder Operationen vordefinierte Bereichsgrenzen nicht überschreiten.

In dem im Folgenden aufgeführten Beispiel hat Polyspace Code Prover festgestellt, dass die Divisionsoperation aus einem Bereich zwischen ‑1701 und 3276 für den linken Operand besteht; der rechte Operand ist 9. Der Bereich, der sich nach der Division ergibt, liegt zwischen -189 und 364.

Tooltip displaying the possible ranges for all run time conditions.

Tooltip, der die möglichen Bereiche für alle Laufzeitbedingungen anzeigt.

Sie können den Steuerungsfluss mit der Aufrufhierarchie und den Aufrufflussdiagrammen visualisieren.

Call flow graph displaying the order of function calls in an interprocedural analysis.

Die Reihenfolge von Funktionsaufrufen in einer Prozessanalyse.

Softwarequalitätsmetriken verfolgen

Sie können ein zentralisiertes Qualitätsmodell definieren, um Laufzeitfehler, Codekomplexität und Verletzungen von Codierungsregeln zu verfolgen. Mithilfe dieser Metrik können Sie den Fortschritt in Bezug auf vordefinierte Softwarequalitätsziele verfolgen, während sich der Code von der ersten Iteration bis hin zur endgültigen Version entwickelt. Durch Messung der Verbesserungsrate bei der Codequalität ermöglicht es Polyspace Code Prover Entwicklern, Testern und Projektmanagern, qualitativ hochwertigen Code bereitzustellen.

Software quality metrics displayed via web browser.

Über den Web-Browser angezeigte Softwarequalitätsmetriken

Codeverifikationsergebnisse zu Simulink-Modellen rückverfolgen

Sie können Polyspace Code Prover für die Verifikation von generiertem Code oder gemischtem Code, der sowohl generierten Code als auch handgeschriebenen Code enthält, verwenden. Bei Fehlern auf Codeebene wird der automatisch generierte Code zum Modell in Simulink rückverfolgt. Sie können erkennen, welche Teile des Modells zuverlässig sind, und Entwurfsprobleme korrigieren, die zu Fehlern im Code führen. Sie können auch mögliche Probleme zwischen der Schnittstelle von generiertem Code und handgeschriebenem Code identifizieren. Beispiel: Der kombinierte Einsatz von handgeschriebenem S-Function-Code und generiertem Code führt möglicherweise zu einem Problem, bei dem nicht korrekte Signalbereiche in der Schnittstelle einen Laufzeitfehler verursachen.

Polyspace Code Prover unterstützt auch die Rückverfolgung von Ergebnissen zu dSPACE® TargetLink®-Blöcken und IBM Rational Rhapsody‑Modellen.

Tracing code verification results to the Simulink model.

Codeverifikationsergebnisse zum Simulink-Modell rückverfolgen.

Codeverifikationsprozess automatisieren

Sie können Polyspace Code Prover als Teil eines kontinuierlichen Integrationsprozesses verwenden, indem Sie Polyspace in Ihren Build-Prozess integrieren. Sie können die Planung von Verifikationsjobs automatisieren und E-Mail-Benachrichtigungen einrichten. Sie können Polyspace Code Prover dazu veranlassen, einem Cluster-Computer Verifikationsjobs zuzuweisen (unter Verwendung von MATLAB Distributed Computing Server). Sie werden per E-Mail benachrichtigt, sobald Ergebnisse verfügbar sind. Ergebnisse enthalten die Unterschiede im Vergleich zur vorherigen Version Ihres Codes. Diese werden vom Server automatisch berechnet.

Sie können festlegen, wie häufig diese Analysen vorgenommen werden sollen, sowie auch das Qualitätsmodell, das auf einen bestimmten Teil der Codebasis angewendet werden soll. Ferner können Sie die E-Mails definieren, die Ihre Anwender erhalten sollen, sobald die Ergebnisse verfügbar sind. Ebenfalls kann definiert werden, welche Erstellungseigenschaften die automatischen Verifizierungen umfassen sollen.

Zertifizierungsartefakte erstellen

Sie können Polyspace Bug Finder und Polyspace Code Prover in Verbindung mit dem IEC Certification Kit (für IEC 61508 und ISO 26262) und DO Qualification Kit (für DO-178B) verwenden, und zwar bei Zertifizierungsvorgängen für Projekte, die auf diesen Industriestandards basieren.

In Berichten und Artefakten wird die Endqualität des Programmcodes angezeigt. Zudem werden überprüfte Abschnitte hervorgehoben, Codemetriken erstellt und die Anwendung von Codierungsregeln und der Laufzeitfehlerstatus dokumentiert. Es ist möglich, diese Berichte im PDF-, HTML- oder RTF-Format und in anderen Formaten zu erstellen.

DO Qualification Kit contents.

Zertifizierungs- und Qualifizierungs-Kits sind verfügbar.

Kein Spaß an Code Reviews? Automatische Verifikation!

Webinar anzeigen