Spezifikation eingebetteter Systeme, Wintersemester 04/05

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
• 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
• Fixpunkttheorie für rekursive Prozesse
• Implizite Spezifikation mit Trace-Zusicherungen

Hintergrundmaterial

• Syntax und Semantic von Timed CSP: pdf
• Beispiel "Die speisenden Philosophen": philosophen.csp
• Beispiel "Bahnübergang": bahn.txt
• Beispiel "Wassertank": waterlevel.txt
• Beispiel "Fischer's Protocol": fischer.txt
• Beispiel für implizite Spezifikation: pdf
• Latex Style-File für implizite Spezifikation: sty

Session 3 - UML

• Übersicht über die UML-Diagramme
• Zustandsdiagramme: Guards, Events, Actions, AND- und OR-States, ...
• Strukturdiagramme: Ports und Konnektoren, Hierarchisierung
• Klassendiagramme mit allen Schikanen
• Anwendungsfalldiagramme

Ü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.
  Achtung:Die aktuelle deutsche Ausgabe behandelt nicht UML 2.0!
• 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, 2003
  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