Polyspace für C/C++-Codeverifikation

In diesem Kurs ermitteln und verbessern Sie die Qualität von eingebetteter Software mittels Polyspace^® Bug Finder^™ und Polyspace Code Prover^™. An unterschiedlichen Punkten des Entwicklungsprozesses spüren Sie potentielle Defekte in C-Code auf und überprüfen den Code auf Richtlinienkonformität. Schließlich weisen Sie nach, dass der Code frei von Laufzeitfehlern ist. Beachten Sie, dass Tag 3 nur bei Schulungen vor Ort optional möglich ist.

Themen sind unter anderem:

Codeanalyse und Codeverifikation im Verlauf von Softwareentwicklungsprozessen
Verstehen und Bewerten von Verifikationsresultaten
Nachbilden des Ausführungskontexts für die Codeverifikation
Nachbilden fehlender Daten und Funktionen
Handhaben von nicht-bewiesenem Code (von den Polyspace^®-Produkten orange markiert)
Überprüfen von MISRA C^®-Konformität
Erzeugen von Reporten

Voraussetzungen

Solide Kenntnisse in C oder C++

Detaillierte Kursbeschreibung anzeigen

Voraussetzungen

Solide Kenntnisse in C oder C++

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: 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

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: 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
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 Erstellen von Dokumenatation

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