Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > WiSe 2008/09 > Deutsch
English
 

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

Vorlesung: 
Do 13 - 15 Uhr MZH 1380 Prof. Dr. Jan Peleska ab 30.10.2008
Übung: 
Di. 8-10 Uhr MZH 1380 Ulrich Hannemann ab 4.11.2008

Überblick

In dieser Veranstaltung werde 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 - 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

Fallstudie zum Umgang mit UPPAAL: Alternating Bit Protocol:

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+

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