Spezifikation eingebetteter Systeme, WiSe 2008/09

Diese Seite gibt weitere Informationen zur Vorlesung. Wir bemühen uns diese Informationen so aktuell wie möglich zu halten.

Aktuelles

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
  • Domänen-spezifische Modellierung auf Grundlage des Graph-Object-Property-Port-Role-Relationship (GOPPRR) Paradigmas. Praktische Anwendungen mit dem Meta-CASE Tool MetaEdit+.
• Systemparadigmen:
  • Zeitgesteuerte (Time-Triggered) Systeme versus
  • ereignisgesteuerte (Event-Triggered) Systeme
• Grundlagen der Modell-basierten Entwicklung (Model-Based Development) für eingebettete Systeme auf Grundlage von Domain-Specific Languages (DSL):
  • Model-to-model transformations
  • Model-to-text transformations, insbesondere model-to-code transformations

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 Automata

• Uhren und Zeitbedingungen
• Region Graph-Semantik
• Das Uppaal Werkzeug
• Spezifikation von Modelleigenschaften mittels Temporaler Logik (wird zusammen mit Session 3 schrittweise eingeführt)
• Modellvalidierung durch Modellprüfung (Property Checking) temporaler Eigenschaften

Hintergrundmaterial

• UPPAAL - editor, simulator and model checker for Timed Automata:
  • Installation instructions
  • Tutorial

• Das Uppaal Modell und
• die zugehörigen Verifikationsbedingungen.

Session 3 - 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

Session 4 - UML für eingebettete Systems

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

Session 5 - DSLs auf Grundlage des GOPPRR Paradigmas

• Abstrakte Syntax und konkrete Syntax
• DSL-Spezifikation mit MetaEdit+
• Transformationssemantiken
• Model-to-text Generatoren zur Modell-basierten Codeerzeugung
  • Transformationsschema DSL --- Generator --- Framework --- Target Code
  • Codegenerierung am Beispiel von Timed Automata

Dazu das Schema der C-Strukturen, mit denen ein Timed Automata modelliert werden kann, und der erste Entwurf eines Generators.

Framework zur Ausführung eines timed automata Modells, Version 2 vom 8. Januar 2009.

Session 6 - Prozessalgebren: 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

Session 7 - Zusicherungen für Prozessalgebren: 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

Übungszettel

• &Aufgabenblatt 1, Abgabe am 20.11.2008
• Aufgabe 2: Ergänzung der graphischen Elemente des Komponentenmodells für timed automata, in der Vorlesung vom 4.12. besprochen, Nachbesprechung am 16. 12.
• Aufgabe 3: Erstellung eines Generators für die Umsetzung der guards, actions und Invarianten in C - Funktionen, in der Vorlesung vm 11.12. besprochen.
• Aufgabenblatt 4: Ergänzung des Frameworks zur Ausführung des timed automata Modells, Erstellen der Interpreter Funktion.

Leistungsnachweise

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.

Domänen-spezifische Modellierung mit MetaEdit+

• Juha-Pekka Tolvanen, Risto Pohjonen and Steven Kelly: Advanced Tooling for Domain-Specific Modeling: MetaEdit+
• Steven Kelly and Juha-Pekka Tolvanen: Domain-Specific Modeling - Enabling Full Code Generation. IEEE Computer Science Publications, John Wiley and Sons, (2008)

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