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ückgaben
  • Identifizierung von Variablen, die vorgegebene Bereichsgrenzen überschreiten
  • Qualitätsmetriken zur Verfolgung der Konformität mit Softwarequalitätszielen
  • Über ein webbasiertes Dashboard können Code-Metrik und Qualitätsstatus angezeigt werden
  • Begleitetes Prüfverfahren zur Klassifizierung von Ergebnissen und Laufzeitfehlerstatus
  • Grafische Anzeige variabler Lese- und Schreibvorgänge

Von Polyspace Code Prover angezeigte Laufzeitfehlerergebnisse


Prüfung von C- und C++-Embedded Software

Polyspace Code Prover führt Codeverifikationen für Embedded Software in C und C++ aus, die höchste Qualitäts- und Sicherheitsstandards erfüllen muss. Das solide Tool für die statische Analyse nutzt eine auf formalen Methoden beruhende Technik namens abstrakte Interpretation, um zuverlässige Verifikationsergebnisse zu liefern. Polyspace Code Prover erkennt, wo Laufzeitfehler auftreten können, und identifiziert Code, der nachweislich sicher vor Laufzeitfehlern ist. Sie verwenden Polyspace Code Prover im Rahmen eines hochwertigen Qualitätssicherungsprozesses, um alle möglichen Kombinationen von Eingaben, Pfaden und Variablenwerten umfassend zu verifizieren. Polyspace Code Prover greift auf eine Farbcodierung zurück, um den Status der einzelnen Code-Elemente anzugeben. Durch die Integration in Simulink® ermöglicht Polyspace Code Prover die Rückverfolgbarkeit von Laufzeitergebnissen auf Codeebene bis zu den Simulink-Modellen.

Polyspace Code Prover bietet Ihnen folgende Möglichkeiten:

  • Bestätigen Ihres Codes: Verifizieren Sie, dass Ihr Code frei von Laufzeitfehlern ist.
  • Ergebnisse ohne falsch negative Ergebnisse: Alle potenziellen Laufzeitfehler werden umfassend identifiziert.
  • Zuverlässige Codequalität: Messung von bewiesenem Code und unbewiesenem Code

Sie können über die Befehlszeile, über eine grafische Benutzeroberfläche oder über Plug-ins für Visual Studio® und Eclipse™ auf Polyspace Code Prover zugreifen. Sie können Polyspace Code Prover einsetzen, um alle kritischen Aktivitäten in einem Softwareentwicklungsworkflow zu unterstützen, wie beispielsweise:

  • das Erkennen von Laufzeitfehlern wie Division durch Null
  • das Nachweisen der Abwesenheit von sicherheitskritischen Laufzeitfehlern wie Pufferüberläufen
  • das Bestimmen von Variablenbereichen und das Sicherstellen, dass keine Bereichsgrenzen verletzt werden
  • das Sicherstellen, dass die jeweiligen Softwarequalitätsziele eingehalten werden
  • das Rückverfolgen von Laufzeitfehlern zu Simulink-Blöcken oder IBM® Rational® Rhapsody®-Modellen
  • das Erstellen von Zertifizierungswerkzeugen

Polyspace Code Prover arbeitet mit Polyspace Bug Finder zusammen, um sicherheitskritische Fehler wie Division durch Null oder sicherheitsrelevante Pufferüberläufe in Ihrem Quellcode zu finden und die Einhaltung von Coding-Standards wie MISRA zu prüfen. Mit diesen Produkten steht eine durchgängige Lösung für die statische Analyse zur Verfügung, die bereits in einem frühen Entwicklungsstadium genutzt werden kann, um Fehler ausfindig zu machen, Codierungsregeln zu prüfen und Laufzeitfehler nachzuweisen. Auf diese Weise lässt sich die Zuverlässigkeit von Embedded Software sicherstellen, die höchste Qualitäts- und Sicherheitsanforderungen erfüllen muss.

Sie können die Codeverifikation beschleunigen und an ein Computer-Cluster auslagern, indem Sie Verifikationsaufträge mit der Parallel Computing Toolbox™ und dem MATLAB Distributed Computing Server™ übermitteln.


Erkennen von Laufzeitfehlern

Polyspace Code Prover setzt auf abstrakte Interpretation mit statischer Codeanalyse, um Laufzeitfehler wie arithmetische Überläufe, Division durch Null und Pufferüberläufe nachzuweisen, zu identifizieren und zu diagnostizieren. Mit dieser Technik lassen sich alle möglichen Laufzeitbedingungen vollständig und umfassend verifizieren. Für jede Codeoperation wird automatisch die Diagnose „bewiesen“, „fehlgeschlagen“, „unerreichbar“ oder „unbewiesen“ gestellt. In den von Polyspace Code Prover produzierten Verifikationsergebnissen ist jede Operation in C oder C++ farbcodiert, um ihren Status anzugeben:

Grün: bewiesenermaßen frei von Laufzeitfehlern
Rot: bewiesenermaßen fehlerhaft bei jedem Ausführen der Operation
Grau: bewiesenermaßen unerreichbar (möglicherweise ein funktionales Problem)
Orange: unbewiesene Operation, die möglicherweise unter bestimmten Bedingungen fehlerhaft ist

Folgende Fehler werden erkannt:

  • Arithmetische Überläufe, Unterläufe, Division durch Null und andere arithmetische Fehler
  • Pufferüberläufe und unerlaubt dereferenzierte Pointer
  • Ständige TRUE/FALSE-Anweisung
  • nicht-initialisierte Klassenmember (C++)
  • Lesezugriff auf nicht-initialisierte Daten
  • Zugriff, um diesen Pointer (C++) für ungültig zu erklären
  • toter Code
  • dynamische Fehler in Bezug auf Objektprogrammierung, Vererbung und Ausnahmebehandlung (C++)

Attribute für von Polyspace Code Prover identifizierte Laufzeitfehler


Anzeige von Bereichsinformationen

Polyspace Code Prover verfolgt den Steuerungs- und Datenfluss durch die Software und zeigt Bereichsinformationen an, die mit Variablen und Operatoren in Zusammenhang stehen. Wenn Sie den Cursor über einem Operator oder einer Variablen platzieren, wird ein Tooltip mit Bereichsinformationen angezeigt. Die formale Methode, die auch als abstrakte Interpretation bezeichnet wird, ermöglicht die Bestimmung genauer Bereichsinformationen, um nachzuweisen, dass die Software frei von bestimmten Laufzeitfehlern wie Division durch Null und Pufferüberläufen ist. Mithilfe von Bereichsinformationen können Sie den Steuerungs- und Datenfluss exakt verfolgen, um Ihre Software zu debuggen oder um sicherzustellen, dass bestimmte Variablen oder Operationen nicht gegen vorgegebene Bereichsgrenzen verstoßen.

Im unten stehenden Beispiel hat Polyspace Code Prover festgestellt, dass die Divisionsoperation aus einem Bereich zwischen -1701 und 3276 für den linken Operanden besteht; der rechte Operand ist 9. Somit ergibt sich nach der Division ein Bereich zwischen -189 und 364.

Sie können den Steuerungsfluss mit der Aufrufhierarchie und den Aufrufflussdiagrammen weiter visualisieren oder die Zugriffe für die Daten Ihrer globalen Variablen anzeigen.

Explore gallery (3 images)


Verfolgung der Softwarequalitätsmetrik

Sie können ein zentralisiertes Qualitätsmodell definieren, um Laufzeitfehler, Codekomplexität und Verletzungen von Codierungsregeln zu verfolgen. Mithilfe dieser Metriken 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 die Messbarkeit der Verbesserungsrate der Codequalität bietet Polyspace Code Prover Entwicklern, Testern und Projektmanagern die Möglichkeit, qualitativ hochwertigen Code zu planen und zu entwickeln.

Über einen Web-Browser angezeigte Softwarequalitätsmetriken.


Sie können Polyspace Code Prover für die Verifikation von generiertem Code oder gemischtem Code, der sowohl generierten als auch handgeschriebenen Code enthält, verwenden. Im automatisch generierten Code gefundene Fehler werden bis zum Modell in Simulink zurückverfolgt. Sie können feststellen, welche Teile des Modells zuverlässig sind, und Entwurfsprobleme beheben, die zu Fehlern im Code führen. Zudem können Sie mögliche Probleme an der Schnittstelle zwischen generiertem und handgeschriebenem Code identifizieren. Die Kombination aus handgeschriebenem S-Function-Code und generiertem Code könnte beispielsweise zu einem Problem führen, bei dem falsche Signalbereiche in der Schnittstelle einen Laufzeitfehler verursachen.

Polyspace Code Prover unterstützt außerdem die Rückverfolgbarkeit von Laufzeitergebnissen zu dSPACE® TargetLink®-Blöcken und IBM Rational Rhapsody-Modellen.

Rückverfolgung der Ergebnisse der Codeverifikation zum Simulink-Modell


Automatisierung des Code-Verifikationsprozesses

Sie können Polyspace Code Prover im Rahmen eines kontinuierlichen Integrationsprozesses nutzen, indem Sie Polyspace in Ihren Build-Prozess integrieren. Sie können die Planung von Verifikationsaufträgen automatisieren und E-Mail-Benachrichtigungen einrichten. Sie können Polyspace Code Prover anweisen, einen Verifikationsauftrag an einen Cluster-Computer zu übertragen (unter Verwendung von MATLAB Distributed Computing Server), und werden dann per E-Mail benachrichtigt, sobald die Ergebnisse verfügbar sind. Die 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, und das Qualitätsmodell angeben, 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. Es kann ebenfalls definiert werden, welche Erstellungseigenschaften die automatischen Verifizierungen umfassen sollen.


Erstellen von Zertifizierungsdokumenten

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

Berichte und Dokumente beinhalten die endgültige Codequalität, heben überprüfte Abschnitte hervor, die generieren Code-Metriken und dokumentieren die Anwendung von Codierungsregeln und Überprüfungen der Laufzeitfehler. Es ist möglich, diese Berichte im PDF-, HTML- oder RTF-Format und in anderen Formaten zu erstellen.

Zertifizierungs- und Qualifizierungskits sind verfügbar.