Spezifikation eingebetteter Systeme, WiSe 2012/13

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

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 - Überblick: Eingebettete Systeme, reaktive Systeme, Model-driven Development

• Eingebettete Systeme
• Reaktive Systeme
  • Semantik zeitlich diskreter Systeme
  • Semantik hybrider (zeitlich diskreter + kontinuierlicher) Systeme
• (Modellierungs-)Formalismen
  • Beschreibung von Struktur, Funktion und nicht-funktionalen Eigenschaften
  • abstrakte / konkrete Syntax
  • Semantik
• implizite / explizite Spezifikation
• Model-driven Development
  • Modell als konkrete Lösung einer (z.B. als Formel) gegebenen Aufgabe
  • Verwendung von expliziter Spezifikation
• Model-driven Development Framework mit DSLs
• DSL-Modell -> Generator -> Code-Fragments
• Code-Fragments + Domain-Framework -> Target
Dazu: MetaEdit+-Beispiel aus der Übung vom 01.11.2010

Session 2 - Berechnungsmodelle und Parallelität

• Modellierung der Zeit
  • Dense-Time-Systems: Timestamps sind positive reelle Zahlen
  • Discrete-Time-Systems: Timestamps sind natürliche Zahlen
• Berechnungsmodelle für zeit-diskrete Systeme
  • Zustandsfolgen: < (s_0,t_0), ..., (s_j,t_j), ... >
    • Valuationsfunktionen s_i : V -> D
    • V : Menge der Symbole, D: Vereinigung der Datentypen über alle Symbole
  • Ereignisfolgen: < (e_0,t_0), ..., (e_j,t_j), ... >
    • Ereignisse e_i aus einem Alphabet E
    • Abstraktion von Zustandsänderungen
  • Ereigniszustandsfolgen: < (s_0,t_0), (s_1,t_1), ..., (e_0,t_n), (e_1,t_n+1), ... >
    • Kombination aus Zustandsfolgen und Ereignisfolgen
• Berechnungsmodelle für hybride Systeme
  • Ereigniszustandsfolgen mit Flow-Conditions: < (s_0,t_0), (e_1,t_1), (s_2,t_2), (s_3,t_3), ... >
    • V: Vereinigung zeitlich diskreter (DIS) und zeitlich kontinuierlicher (CONT) Variablen
    • Valuationsfunktionen s_i: V -> D
    • Flow-Conditions delta_i : CONT x (0,t_i+1-t_i) -> R
    • für v aus CONT: s_i(v), s_i+1(v) sind Werte von v zu Zeitpunkten t_i bzw. t_i+1
    • für v aus CONT: delta_i(v,tau) ist Wert von v zum Zeitpunkt t_i < t_i+tau < t_i+1
• Klassifikation von Zustandsübergängen
  • in V: Unterscheidung zwischen Inputs und sonstigen Symbolen
  • diskrete Transitionen ändern den Zustand, jedoch nicht die Zeit oder Inputs
  • Delay-Transitionen ändern die Zeit und/oder Inputs, jedoch nicht den sonstigen Zustand
• Semantische Modelle der Parallelität
  • True Parallelism: echte Parallelität
  • Interleaving Semantik: Kausalordnung von Zustandsänderungen ist immer gegeben
• Kommunikation und Synchronisation
  • Shared Variables
  • Synchrone Events (Handshake)
  • Synchrones Message Passing: Events und Shared Communication Variables
  • Asynchrones Message Passing: Verwendung von gepuffertem synchronem Message Passing

Session 3 - Timed Automata in UPPAAL

• Zeitmodell, UPPAAL-Systeme, UPPAAL-Prozesse
• Synchronisation zwischen Prozessen
• Simulation von Modellverhalten
• Prüfung von Modelleigenschaften

Hintergrundmaterial

• UPPAAL Download
• UPPAAL Dokumentation und Tutorials

Session 4 - Meta Case Tools: Entwurf neuer Modellierungsformalismen

• Meta-Meta-Modell --- Meta-Modell --- Modell --- Code
  • Konkurrierende Meta-Meta-Modelle: MOF, GOPPRR, Ecore
  • Model-to-Text Transformationen
  • Model-to-Model Transformationen
• DSL-Spezifikationen mit MetaEdit+
  • Beispiel: hierarchisch aufgebaute Netzwerke von Timed Automata
  • Spezifikation einer Modellierungssprache
  • Spezifikation eines Codegenerators mit MERL (MetaEdit+ Reporting Language)
• Ausdrucksmächtigkeit von EBNF vs. GOPPRR
  • EBNF-Spezifikation als Syntaxgraph
  • GOPPRR-Modell zur Definition von Syntaxgraphen
  • Syntaxprüfung mit Hilfe von Generatoren

Session 5 - Workflow: vom DSL-Modell zum Ausführbarer Code

• Modelltransformationen: Design-Patterns
  • Visitor-Pattern
  • Composite-Pattern
• Workflow
  • DSL-Modell ⇒ Generator/Export ⇒ Modell-Text
  • Modell-Text ⇒ libxml2/Lex/Yacc/C++ ⇒ Modell-AST
  • Modell-AST ⇒ Code-AST
  • Code-AST ⇒ Code

Hintergrundmaterial

• Folien und Code-Beispiele aus dem libxml2-Tutorium (Helge Löding, 31.01.2011)

Übungszettel

Leistungsnachweise

1. Erreichen von mind. 60% über alle Übungszettel (in Gruppen von 2-4 Studierenden) und Bestehen des anschließenden Fachgesprächs
2. Bestehen einer Modulprüfung

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 Society 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