Polyspace für C/C++-Codeverifikation

Tag 1 von 3

Überblick über Polyspace-Prozesse

Ziel: Verstehen an welcher Stelle im Softwareentwicklungsprozess Polyspace Bug Finder und Polyspace Code Prover richtigerweise eingesetzt werden. Vertraut machen mit den Produkten anhand der Analyse eines einfachen C-Programms.

• Softwareentwicklungsprozesse mit Polyspace
• Einführendes Beispiel zur Codeverifikation
• Analyse von Defekten und Laufzeitfehlern

Codeanalyse mit Polyspace Bug Finder

Ziel: Analysieren von Code, der nicht ANSI-C konform ist. Berücksichtigen der Laufzeitumgebung und des Ausführungskontexts und korrigieren von Defekten und Verletzungen von Code-Regeln mit Polyspace Bug Finder.

• Typische Artefakte einer Laufzeitumgebung
• Verifizieren von prozessorspezifischem Code
• Definieren des Ausführungskontext
• Berücksichtigen der Zielhardware
• Analysieren und Handhaben von Defekten
• Aufspüren von Programmierrichtlinienverletzungen
• Erfassen von Codemetriken

Analysieren von Polyspace Code Prover-Ergebnissen

Ziel: Nutzen verschiedener Werkzeuge des Polyspace Code Prover, um durch die Ergebnisse des Polyspace Code Prover zu navigieren, und um diese zu interpretieren.

• Überblick über die abstrakte Interpretation
• Analysieren des Aufrufbaums
• Navigieren durch den Quellcode
• Analysieren der Ausführungspfade
• Untersuchen der Wertebereiche von Variablen
• Analysieren der Zugriffe auf globale Variablen

Checks zur Codeverifikation

Ziel: Nutzen verschiedener Werkzeuge des Polyspace Code Prover, um durch die Ergebnisse des Polyspace Code Prover zu navigieren, und um diese zu interpretieren.

• Überblick über die abstrakte Interpretation
• Analysieren des Aufrufbaums
• Navigieren durch den Quellcode
• Analysieren der Ausführungspfade
• Untersuchen der Wertebereiche von Variablen
• Analysieren der Zugriffe auf globale Variablen

Tag 2 von 3

Bewerten von Verifikationsergebnissen

Ziel: Handhaben von Ergebnissen mit zahlreichen unbewiesenen Checks.

• Bestimmen des Verifikationsaufwands
• Durchführen eines schnellen Reviews
• Untersuchen ausgewählter unbewiesener Checks
• Einstellen der Verifikationsgenauigkeit
• Priorisieren unbewiesener Checks
• Durchführen eines Reviews unbewiesener Checks

Präzisieren von Verifikation mit Polyspace Code Prover

Ziel: Handhaben von Ergebnissen mit zahlreichen unbewiesenen Checks.

• Bestimmen des Verifikationsaufwands
• Durchführen eines schnellen Reviews
• Untersuchen ausgewählter unbewiesener Checks
• Einstellen der Verifikationsgenauigkeit
• Priorisieren unbewiesener Checks
• Durchführen eines Reviews unbewiesener Checks

Integrationsanalyse

Ziel: Analysieren und Beheben von Problemen, die sich bei der Codeintegration mehrerer zusammenhängender Softwaremodule ergebenden.

• Verwalten von Modulen
• Analysieren von sich bei der Integration ergebenden Defekten und Richtlinienverletzungen mit Polyspace Bug Finder und Polyspace Code Prover
• Importieren von Reviewinformationen

Analyse einer kompletten Applikation

Ziel: Anwenden verschiedener Verfahren und Optionseinstellungen um den kompletten Code einer Applikation zu analysieren.

• Aufsetzen einer Applikationsverifikation
• Verbessern der Ergebnisse einer Applikationsverifikation
• Aufspüren von Problemen mit Nebenläufigkeit
• Vergleichen von robuster und kontextueller Verifikation
• Dokumentieren von Ergebnissen

Tag 3 von 3

Hands-On Übungen (nur bei Vor-Ort-Schulungen)

Ziel: Anwenden des Gelernten auf den eigenen Code und integrieren von Polyspace Bug Finder und Polyspace Code Prover in einen Entwicklungsprozess. Mögliche Themen sind:

• Polyspace Bug Finder-Checks
• Verifikation von C++-Code
• Nebenläufigkeit und Analyse gemeinsamer Variablen
• Verifikation automatisch generierten Codes
• Review des Entwicklungsprozesses
• Prozessintegration
• Client/Server-Installation
• Polyspace für ein Projekt konfigurieren
• Interpretation der Ergebnisse