Verifikation digitaler Systeme - Cheatsheet

Grundlagen der formalen Spezifikation

Definition:

Verwendung mathematischer Methoden zur präzisen Beschreibung des Verhaltens digitaler Systeme.

Details:

• Mathematische Modelle: Automaten, Zustandsräume, formale Logik.
• Spezifikationssprachen: Z, VDM, B.
• Ziel: eindeutige, überprüfbare und analysierbare Spezifikationen.
• Wichtige Begriffe: Prädikat, Invariante, Konsistenz, Vollständigkeit.
• Verwendung von formalen Methoden zur Verifikation und Validierung.

Model Checking Algorithmen zur Zustandsraumerkundung

Definition:

Model Checking Algorithmen untersuchen Zustandsräume digitaler Systeme, um zu überprüfen, ob sie die spezifizierten Eigenschaften erfüllen.

Details:

• Zustandsexplosion: Größe des Zustandsraums exponentiell in der Anzahl der Variablen.
• Graphbasierte Verfahren: Durchlaufe alle Zustände und Übergänge.
• Breadth-First Search (BFS): Erkundet Zustandsraum Ebene für Ebene.
• Depth-First Search (DFS): Verfolgt jeden Zustandspfad bis zum Ende.
• Symbolisches Model Checking: Nutzung von BDDs zur kompakten Zustandsraumdarstellung.
• Temporal Logic: Überprüfung von Eigenschaften in der Zeit (LTL, CTL).
• Formale Spezifikation: Zu überprüfende Eigenschaften spezifiziert in temporaler Logik.
• Automatisierte Verifikation: Model Checker führt die Verifikation automatisch durch.

Lineare temporale Logik (LTL) und Berechnungsbaumlogik (CTL)

Definition:

LTL: Formale Sprache zur Spezifikation von Temporaleigenschaften von Systemen. CTL: Erweiterung der temporalen Logik zur Spezifikation von Eigenschaften auf Verzweigungsmodellen.

Details:

• LTL: Betrachtet lineare Abfolgen von Zuständen, Operatoren: X (Next), G (Globally), F (Finally), U (Until)
• CTL: Betrachtet verzweigende Abfolgen von Zuständen, Operatoren: A (Alle Pfade), E (Es gibt einen Pfad), sowie LTL-Operatoren in Kombination
• LTL Syntax: \texttt{X} p, \texttt{G} p, \texttt{F} p, p \texttt{U} q
• CTL Syntax: \texttt{AX} p, \texttt{EX} p, \texttt{AG} p, \texttt{EG} p, \texttt{AF} p, \texttt{EF} p, \texttt{A} (p \texttt{U} q), \texttt{E} (p \texttt{U} q)
• LTL fokussiert auf Sequenzen von Zuständen (linear).
• CTL fokussiert auf Zustandsbäume (verzweigt).
• Unterschied LTL/CTL: LTL beschreibt nur lineare Referenzpfade, CTL beschreibt alle möglichen Pfade im Modells.

Symbolic Model Checker (SMV) Einsatz

Definition:

Verwendung von SMV zur systematischen Überprüfung digitaler Systeme mittels symbolischer Modellprüfung

Details:

• Verifiziert Finite-State-Maschinen (FSMs) und digitale Schaltungen
• Sprache: SMV (Symbolic Model Verifier)
• Einsatz in der Vorlesung 'Verifikation digitaler Systeme', Informatik, Universität Erlangen-Nürnberg
• Überprüft Eigenschaften wie Sicherheit und Liveness
• Repräsentation von Zustandsräumen durch BDDs (Binary Decision Diagrams)
• Formalisierung von Anforderungen in temporaler Logik: CTL (Computation Tree Logic) oder LTL (Linear Temporal Logic)
• Ergebnisse: Validierungsoutput [true/false] und Gegenbeispiele bei Fehlverhalten

Verwendung von SPIN zur Protokollverifikation

Definition:

Verwendung von SPIN zur Protokollverifikation - SPIN ist ein Model-Checker zur Verifikation von Kommunikationsprotokollen und verteilten Systemen.

Details:

• SPIN = Simple Promela Interpreter
• Model-Checking zur Verifikation der Korrektheit von Protokollen
• Verwendung von Promela (Process Meta Language) zur Spezifikation
• Überprüfung auf Deadlocks, unzulässige Zustände, Livelocks
• Übliche Schritte: Modellierung in Promela, Formulierung von Eigenschaften in Linear Temporal Logic (LTL), Durchführung des Model-Checkings

Fehlerinjektion und Fehlersuche

Definition:

Fehlerinjektion: Methode zur Erzeugung künstlicher Fehler zur Beobachtung des Systemverhaltens. Fehlersuche: Systematisches Identifizieren und Beheben von Fehlern im digitalen System.

Details:

• Fehlerinjektion:
• Verwendung: Validierung, Test und Bewertung von Fehlertoleranz
• Techniken: Hardware-basierte, Software-basierte und Simulationstechniken
• Beispiele: Störung von Bits in Speichern, Störung von Signalen auf Bussen
• Fehlersuche:
• Verwendung: Debugging, Verifikation und Validierung
• Techniken: Manuelles Debugging, automatisierte Analysetools
• Ansätze: Top-Down (System zu Komponenten), Bottom-Up (Komponenten zu System), und Hybridmethoden
• Tools: Debugger, Logikanalysatoren, Emulatoren

Praxisnahe Übungen zur Modellierung und Verifikation

Definition:

Praxisbezug durch Übungen zur Modellierung und Verifikation digitaler Systeme im Kurs 'Verifikation digitaler Systeme'.

Details:

• Verwendung von Modellierungswerkzeugen und -sprachen (z.B. VHDL, Verilog).
• Einsatz formaler Verifikationsmethoden (z.B. Model Checking, Theorem Proving).
• Praktische Umsetzung und Analyse von Beispielen aus der Industrie.
• Fehlererkennung und -korrektur in digitalen Systemen.
• Format: Übungen im Labor oder als Praktikumsaufgaben.

Einsatz von Theorem Provers bei der Verifikation

Definition:

Einsatz formaler Beweissysteme zur automatisierten Überprüfung der Korrektheit digitaler Systeme.

Details:

• Nutzung mathematischer Logik zur Modellierung und Verifikation
• Beweisführung: - Existenzbeweis (Existenz von Lösungen) - Ungültigkeitsbeweis (Nicht-Existenz von Lösungen)
• Wichtige Werkzeuge: Isabelle, Coq, HOL
• Input: Modell des digitalen Systems (z.B. Schaltkreisbeschreibung, Algorithmen)
• Output: Formale Beweise zur Systemkorrektheit
• Vorteile: Hohe Zuverlässigkeit, formale Sicherheit
• Nachteile: Hoher initialer Aufwand, Komplexität des Beweises kann hoch sein
• Anwendungsbereiche: Sicherheitssensitive Systeme, Mikrochips, Softwareverifikation