Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > WiSe 2012/13 > Deutsch
English
 

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

Vorlesung: 
Fr. 14-16 Uhr, MZH 1450 Prof. Dr. Jan Peleska
Übung: 
Fr. 16-18 Uhr, MZH 1450 Prof. Dr. Jan Peleska

Überblick

In dieser Veranstaltung werden Spezifikationsformalismen eingeführt, die besonders für die Beschreibung von eingebetteten Steuerungssystemen mit Echtzeitbedingungen geeignet sind. Wir führen in Paradigmen, d.h. wiederkehrende Grundmuster, ein, nach denen typische Anforderungen an Echtzeitsysteme klassifiziert und beschrieben werden können und geben eine Übersicht über die aktuellen Forschungsthemen auf diesem Gebiet.

  • 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

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


Übungszettel


Leistungsnachweise

Um einen Leistungsnachweis für diese Veranstaltung zu erhalten, werden zwei Optionen angeboten:
  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+

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

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

 
   
Autor: jp
 
  AG Betriebssysteme, Verteilte Systeme 
Zuletzt geändert am: 2. November 2022   Impressum