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

Ziel: Analysieren von Code, der nicht ANSI-C konform ist. Berücksichtigen der Laufzeitumgebung und des Ausführungskontexts.

• 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

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

Ziel: Untersuchen von Verifikationsergebnissen, um das Verhalten der unterschiedlichen Checks kennenzulernen, und um Polyspace Code Prover zu Ihrem Entwicklungsprojekt passend zu konfigurieren.

• Überblick über C-Quellcode-Checks
• Lokalisieren der Checks im Quellcode
• Interpretieren der Checkbeschreibungen
• Einstellen relevanter Optionen

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

Ziel: Anpassen der Art und Weise mit der Polyspace Code Prover fehlenden Code behandelt, um die Verifikation eines Softwaremoduls sinnvoll zu präzisieren.

• Einfluss von fehlendem Aufrufkontext auf die Verifikation
• Stubben von Funktionen
• Einschränken von Wertebereichen
• Schreiben von manuellen Funktionsstubs

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

Ziel: Sammeln der Verifikationsergebnisse im Polyspace Metrics Server und Erstellen von Berichten, um die Ergebnisse zu dokumentieren und an Dritte zu verteilen.

• Verteilen von Ergebnissen
• Verwenden von Polyspace Metrics
• Überprüfen des Software-Qualitätsniveaus
• Erstellen von Dokumentation

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

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:

• Review des Entwicklungsprozesses
• Prozessintegration
• Client/Server-Installation
• Polyspace für ein Projekt konfigurieren
• Interpretation der Ergebnisse