Spezifikation eingebetteter Systeme, Sommersemester 2006

Aktuelles

• Abgabe des dritten Zettels bis zum 29.6. verlängert! Der vierte Aufgabenzettel wird ebenfalls am 29.6. erscheinen.
• tcsp.pdf aktualisiert!

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Übungszettel
• Leistungsnachweise
• Literatur

Termine

Überblick

• Spezifikationsformalismen:
  • Ausdrucksmächtigkeit
  • Semantik und Anwendung an Beispielen aus dem Gebiet Echtzeitsysteme: Timed Automata, Timed CSP, Hybrid Statecharts für Systeme mit diskreten und analogen Steuerungsgrößen, UML-Diagrammtypen mit Eignung für Echtzeitsysteme, Temporallogik
• Systemparadigmen:
  • Zeitgesteuerte (Time-Triggered) Systeme versus
  • ereignisgesteuerte (Event-Triggered) Systeme
• Basismechanismen für Echtzeitbetriebssysteme zur Umsetzung von Spezifikationen in ausführbare Hardware/Software-Systeme

Veranstaltungsinhalte

Session 1 - Rückblick auf Endliche Deterministische Automaten

• Reaktive Systeme
• Eingebettete Systeme
• Endlicher, deterministischer Automat:
  • endliche Menge von Zuständen K
  • Alphabet Sigma
  • Transferfunktion delta KxSigma->K
  • Initialzustand s, Element von K
  • Menge der Endzustände F, Teilmenge von K
• Syntax und Semantik eines EDA
• Systemausführung (Run/Execution/Computation) eines EDA, Folge der "relevanten" Beobachtungen eines Systemverhaltens
• Was zur Spezifizierung eingebetteter Systeme im Gegensatz dazu benötigt wird:
  • unendlicher Zustandsraum zur Beschreibung reellwertiger Zustände
  • Funktionen über der Zeit zur Beschreibung kontinuierlichen Verhaltens
  • Zeitbedingungen
  • statistische Bedingungen für Transitionen
  • Parallelität
  • unendliche Runs

Session 2 - Timed CSP

• Syntax von Timed CSP:
  
  • STOP, SKIP,
  • a -> P, P [] P, P |~| P,
  • P ; P, P ||| P, P [| H |] P,
  • P\H,
  • Timeout-Operator
  • ...
• Kommunikation über Events, zusätzliche Events für Terminierung und leeres Event
• global physical clock, Timestamps aus R+
• Wait-Prozess
• Runs von Timed CSP-Prozessen: Timed Traces
• Finite Variability, None-zeno Property
• Darstellung als Timed Transition System (TTS)
• Operationelle Semantik
• Strukturelle Dekomposition
• Ausführbarkeit von TCSP-Spezifikationen

Hintergrundmaterial

• Beispiel "Die speisenden Philosophen": philosophen.csp
• Syntax und Semantic von Timed CSP: pdf
• Hinweise zur Verwendung für FDR für untimed CSP
• Beispiel "Cigeratte's Smoker Problem": smokers.csp
• Beispiel "Wassertank": waterlevel.txt
• Beispiel "Fischer's Protocol": fischer.txt

Session 3 - Trace Logic

• Implizite Spezifikation mit Trace Logic
• Finite traces tr
• Timed Traces s
• Erfüllen von Prädikaten: Process sat P(tr)
• Syntax für Operatoren auf Sequenzen
  • Konkatentieren von Sequenzen
  • head(seq), tail(seq), foot(seq), init(seq)
  • Länge der Sequenz: #seq
  • Element an Stelle i: seq@i
  • ...
• Syntax für Operatoren auf timed traces
  • Restriktion von timed traces
  • Sequenz ohne Zeit: strip(s)
  • begin(s), end(s), first(s), last(s)
  • Restriktion auf Intervalle
  • ...
• Makros für timed traces
  • a zum Zeitpunkt t: a at t
  • a im Intervall I: a at I
  • Event aus A im Intervall I: A at I
  • kein Event aus A in der timed trace: no A
  • nur Events aus A in der timed trace: only A

Hintergrundmaterial

• Beispiel für implizite Spezifikation: pdf
• Latex Style-File für implizite Spezifikation: .sty
• Syntax für Trace Logic: pdf

Session 4 - Temporale Logiken

• Spezifikation von Safety-Eigenschaften
• Spezifikation von Liveness-Eigenschaften
• Linear Trace Logic(LTL)
• Computational Tree Logic (CTL)
• Modell: Transitionssystem TS=(s, s0, T,X) mit X Menge der Variablensymbole
• Syntax von CTL:
  • always/globally: G p
  • eventually/finally: F.p
  • until: p U q
  • next: Xq
  • Für alle Ausführungsfolgen ab dem aktuellen Zustand: A q
  • Es existiert eine Auführungsfolge ab dem aktuellen Zustand: E q

Hintergrundmaterial

Session 5 - UML

• Übersicht über die UML-Diagramme
• Zustandsdiagramme: Guards, Events, Actions, History,...
• Strukturdiagramme: Ports und Konnektoren, Hierarchie
• Klassendiagramme: Klassen, Assoziationen, Enums, Interfaces
• Use Cases
• Sequenzdiagramme
• ...

Hintergrundmaterial

• Beispiel aus der Übung vom 18.7.: Use Case
• Beispiel aus der Übung vom 18.7.: Klassendiagramm
• Beispiel aus der Übung vom 18.7.: Strukturdiagramm
• Beispiel aus der Übung vom 18.7.: Sequenzdiagramm 1
• Beispiel aus der Übung vom 18.7.: Sequenzdiagramm 2

Übungszettel

Leistungsnachweise

• Entweder durch erfolgreiches Bearbeiten von Übungsaufgaben inkl. bestandenem Fachgespräch,
• oder durch eine bestandene mündliche Prüfung (alias mündliche Modulprüfung).

Die genauen Bedingungen werden in der ersten Vorlesung verhandelt.

Literatur

Real-Time Systems

• Hermann Kopetz:
  Real-Time Systems, Design Principles for Distributed Embedded Applications,
  Kluwer Academic Publishers, 1997
  Behandelt Grundlagen wie z.B. die Unterscheidung in time-triggered und event-triggered Systeme.

UML

• James Rumbaugh, Ivar Jacobson, Grady Booch:
  The Unified Modeling Language Reference Manual, Second Edition,
  Addison-Wesley Professional, 2004
  UML 2.0 Referenzbuch.
• Martin Fowler:
  UML Distilled, Third Edition,
  Addison-Wesley Professional, 2003
  UML 2.0 in aller Kürze.
• Martin Fowler:
  UML konzentriert,
  3. aktualisierte Auflage,
  Addison-Wesley, 2003
  Achtung:Die Übersetzung soll nicht soooo gelungen sein!
• UML 2.0 Superstructure Specification,
  OMG, 2005
  Die Spezifikation - für die ganz Harten.

CSP und Timed CSP

• C.A.R. Hoare:
  Communication Sequential Processes,
  Prentice Hall, 1986
  Zur Vertiefung von Untimed CSP.
• Steve Schneider:
  Concurrent and Real-Time Systems,
  John Wileyan and Sons Ltd, 2000
  Das Buch zu Timed CSP.

Timed Automata

• Rajeev Alur, David L. Dill:
  A Theory of Timed Automata,
  Theoretical Computer Science, Volume 126, No 2, 1994
  DAS Paper zu Timed Automata.

Hybrid Automata

• Thomas A. Henzinger:
  The Theory of Hybrid Automata,
  Proceedings LICS 1996, IEEE Computer Society Press, 1996
  DAS Paper zu Hybrid Automata.
• Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine:
  The algorithmic analysis of hybrid systems,
  Theoretical Computer Science, Volume 138, 1994
  Nette Übersicht mit vielen Beispielen.
• R. Alur, T. Dang, J. Esposito, R. Fierro, Y. Hur, F. Ivancic, V. Kumar I. Lee, P. Mishra, G. Pappas, O. Sokolsky:
  Hierarchical Hybrid Modeling of Embedded Systems,
  Proceedings EMSOFT, 2001
  Hybrid und hierarchisch.
• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska:
  HybridUML Profile for UML 2.0,
  SVERTS, workshop hold in conjunction with UML 2003, 2003
  Auch die Veranstalter spielen mit Hybrid Automata ;-)
• Kirsten Berkenkötter, Stefan Bisanz, Ulrich Hannemann, Jan Peleska:
  Executable HybridUML and Its Application to Train Control Systems,
  Springer LNCS 3147, 2004
  Unsere "neuesten" Erkenntnisse zu HybridUML

Temporallogik

• Zohar Manna, Amir Pnueli:
  The Temporal Logic of Reactive and Concurrent Systems, Specification,
  Springer, 1991
  Grundlagenbuch zu temporalen Logiken.
• Zohar Manna, Amir Pnueli:
  Temporal Verification of Reactive Systems, Safety,
  Springer, 1995
  Vertiefung