Vorlesungsfolien - Protocol Engineering

Kapitel 1

Abschnitt 1 (25.03.2015)

  • I. Motivation
  • I.1 Warum Protocol Engineering ?
  • I.2 Elemente der Beschreibung von Kommunikationsdiensten und -protokollen
  • I.2.1 Dienstspezifikation
  • I.2.2 Protokollspezifikation
  • I.3 Probleme der Nutzung formaler Beschreibungstechniken

Abschnitt 1, hochkant ()

Kapitel 2

Abschnitt 1 (28.04.2015) - aktualisiert

  • II. Formale Beschreibungsmethoden und -techniken
  • II.1 Formale Beschreibungsmethoden
  • II.2 Formale Beschreibungstechniken
  • II.3 Methoden und Techniken der formalen Beschreibung
  • II.3.1 Automatenorientierte Beschreibung
  • II.3.2 Ablauforientierte Beschreibung MSC (Message Sequence Charts)

Abschnitt 1, hochkant (27.04.2015)

Abschnitt 2 (11.05.2015) - aktualisiert

  • II.3.3 Petri-Netze
  • II.3.4. Algebraische Beschreibungen

Abschnitt 3 (01.06.2015) - aktualisiert

  • II.3.5 Temporale Logiken
  • II.3.6 Hybride Methoden
  • II.3.7 Datenbeschreibung Beispiel: ASN.1 (Abstract Syntax Notation One)
  • II.3.8 UML-2 (Unified Modeling Language)

Kapitel 3

Abschnitt 1 (01.06.2015)

  • III. Protokollentwicklungsprozess
  • III.1 Entwicklungsphasen
  • III.2 Spezifik der Protokollentwicklung

Abschnitt 1, hochkant (01.06.2015)

Kapitel 4

Abschnitt 1 ()

  • IV. Entwurf
  • IV.1 Systematischer Protokollentwurf
  • IV.2 Spezifikation

Abschnitt 1, hochkant ()

Kapitel 5

Abschnitt 1 ()

  • V. Protokollverifikation
  • V.1 Ziele der Protokollverifikation
  • V.2 Verifikationstechniken
  • V.3 Erreichbarkeitsanalyse (Reachability Analysis)
  • V.3.1 Erzeugung des Erreichbarkeitsgraphen
  • V.3.2 Analysen
  • V.3.3 Zustandsraumexplosion

Abschnitt 1, hochkant ()

Abschnitt 2 ()

  • V. Protokollverifikation (Fortsetzung)
  • V.4 Petri Netz-Analyse
  • V.5 Verifikation algebraischer Spezifikationen
  • V.5.1 Äquivalenzanalysen
  • V.5.2 Bisimulation
  • V.5.3 Wichtige Äquivalenzrelationen

Abschnitt 3 ()

  • V.6 Temporallogisches Schließen
  • V.7 Model Checking
  • V.7.1 Model Checker für verzweigende temporale Logiken
  • V.7.2 Model Checker für lineare temporale Logiken

Abschnitt 3, hochkant ()

Kapitel 6

Abschnitt 1 ()

  • VI. Implementierung
  • VI.1 Von der Protokollspezifikation zur Implementierung
  • VI.2 Implementierungsmodelle
  • VI.2.1 Server-Modell
  • VI.2.2 Activity Thread-Modell
  • VI.3 Schnittstellengestaltung
  • VI.4 Spezifische Implementierungsprobleme

Abschnitt 2

  • VI. Implementierung (Fortsetzung)
  • VI.5 Spezielle Implementierungstechniken
  • VI.5.2 Integrated Layer Processing (ILP)
  • VI.6 Automatische Protokollimplementierung

Abschnitt 2, hochkant

Kapitel 7

Abschnitt 1

  • VII. Protokolltest
  • VII.1 Konformitätstest (Conformance test)
  • VII.1.1 Prinzip des Konformitätstest
  • VII.1.2 OSI-Konformitätstestmethodik
  • VII.1.3 Testarchitekturen/-methoden
  • VII.2 Zertifizierung

Abschnitt 1, hochkant

Abschnitt 2

  • VII.3 Ableitung von Testfällen
  • VII.3.1 Fehlermodell
  • VII.3.2 Methoden der Testfallableitung
  • VII.3.3 Ableitung von Testfällen aus formalen Beschreibungen
  • VII.4 Interoperabilitätstest (Interoperability test)

Abschnitt 3

  • VII.4 Testbeschreibungssprachen
  • VII.4.1 TTCN-2 (Tree and Tabular Combined Notation)
  • VII.4.2 TTCN-3 (Testing and Test Control Notation)