Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > SoSe 2006 > Deutsch
English
 

Spezifikation eingebetteter Systeme, Sommersemester 2006

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

Aktuelles

  • Abgabe des dritten Zettels bis zum 29.6. verlängert! Der vierte Aufgabenzettel wird ebenfalls am 29.6. erscheinen.
  • tcsp.pdf aktualisiert!

Inhalt dieser Seite


Termine

Vorlesung: 
Mo. 8-10 Uhr GW2 B2890 Prof. Dr. Jan Peleska ab 24.4.2006
Übung: 
Di. 8-10 Uhr MZH 7260 Kirsten Berkenkötter ab 25.4.2006

Ü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
  • 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
  • Strukturelle Dekomposition
  • Ausführbarkeit von TCSP-Spezifikationen

Hintergrundmaterial

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

Hintergrundmaterial

  • Beispiel für implizite Spezifikation: pdf
  • Latex Style-File für implizite Spezifikation: .sty
  • Syntax für Trace Logic: pdf

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

Hintergrundmaterial

Session 5 - UML

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

Hintergrundmaterial

Übungszettel

Übungszettel Ausgabe Abgabe
Serie 1 8.5.2006 22.5.2006
Serie 2 22.5.2006 6.6.2006
Serie 3 12.6.2006 29.6.2006
Serie 4 29.6.2006 10.7.2006
Serie 5 10.7.2006 24.7.2006

Leistungsnachweise

Einen benoteten Leistungsnachweis erhaltet Ihr bei erfolgreich erbrachter Prüfungsleistung:
  • 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.
  • 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.

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