Lectures
Bernhard
Schätz
Vorlesung "Spezifikation verteilter Systeme"
Leopold-Franzens Universität Innsbruck
Typ: VU 2 (siehe auch
LZK 703616)
Zeit: Montag, 10:00 - 12:00 (1.Termin: 07.03.2005)
Ort: E.heim 3
Achtung:
Ab 11.04.2005 in HS 10, Gebäude 4 (Architektur)
Klausur
Termin: 06.07.2005, 10:00 -
12:00
Ort: Technik/Informatik&ZID
/ Hörsaal 11
Hilfsmittel: Skript,
Vorlesungsmitschriften, Fachliteratur, Foliensätze (Achtung: Aktuellen Satz vom 30.06.2005
verwenden!)
Klausurergebnisse
Klausurangabe: PDF-Version (Punktezahl ist
vorläufig)
Musterlösung: PDF-Version
(Punktezahl ist vorläufig)
Die Ergebnisse der Klausur werden ab dem 16.08.2005 hier
veröffentlicht.
Um Überschneidungen mit anderen Prüfungen zu vermeiden, wird
eine Wiederholungssprüfung am 15.11.2005 angeboten. Bitte melden
Sie sich bis zum 01.11.2005 per email an.
Vorlesungsinhalt
Die Vorlesung stellt einige der elementaren Ansätze vor, die
in vielen der heute verwendeten Techniken zur Realisierung
interagiernder
Systeme zum Einsatz kommen. Themenschwerpunkte sind dabei die
Spezifikation
von Interaktion, Koordination, und Kommunikation. Für alle
Themenblöcke
werden neben den Grundlagen auch Bezüge zu aktuellen
Anwendungsbereichen
dieser Grundlagen (z.B. synchrone Sprachen,
Geschäftsprozessmodellierung,
Protokollmodellierung) hergestellt.
Themen
- Introduction
- Basics
Models: Transition systems
Topics: Computation, interaction, concurrency
- Coroutines
Models: Shared Variables
Topics: State, interference
Examples: Threads, semaphors
- State-Based Models
Models: Automata
Topics: Hierarchic descriptions
Examples: AutoFocus, Statecharts
- Communication
Models: CSP, CCS
Topics: Synchronous communication, process algebras
Examples: occam, RPC
- Data Flow Models
Models: Transition systems, Kahn networks
Topics: Asynchronous communication
Examples: SDF, SDL
- Coordination
Models: Petri nets
Topics: P/E-nets, invariant, reachability
Examples: Activity diagrams, BEPL
- Executions
Models: Event structures
Topics: Executions and automata
Examples: Sequence diagrams, collaboration diagrams
- Properties
Models: Kripke structures
Topics: CTL, LTL, safety, lifeness
Examples: Model Checking
Übungen
In der begleitenden Übung werden die in der Vorlesung
vorgestellten Prinzipien und Ansätze anhand von
Anwendungsbeispielen diskutiert;
stellenweise werden dazu frei verfügbare Modellierungswerkzeuge
eingesetzt.
Unterlagen
Begleitende Unterlagen werden hier im Laufe des Semesters zur
Verfügung gestellt. Die Folien sind vorläufig und werden nach
Abschluss des Semesters nochmals überarbeitet. (Letzter Update: 30.06.2005).
1. Introduction
2. Basics - Transition Systems *
Transition Systems -
Exercises and Questions
Basics - Traces
Traces - Exercises and
Questions
Basics
- Event Structures
Event Structures -
Exercises and Questions
Basics -
Kripke Structures
3. Coroutines
Exercises and Questions
4. Synchronous Data Flow
Synchronous Data Flow -
Exercises and Questions
Asynchronous
Data Flow
Asynchronous Data Flow -
Exercises and Questions
5. Communicating Processes
Communicating
Processes - Exercises and Questions
6. Coordination *
Coordination - Exercises
and Questions
7. Executions
8. Properties
Properties
- Exercises and Questions
9. Implementation
Werkzeuge
Einige frei verfügbare Werkzeuge für Modellierung verteilter
Systeme
- AutoFocus (Erweiterte
Synchronisierte Automaten)
- LTSA
(CSP, Synchrone Transitionssysteme)
- PEP
(Petrinetze)
- Ptolemy
(Hybride Systeme)
Literatur
P. Marwedel. Embedded System Design. Kluwer Acad. Publ, 2003.
J. Magee, J. Krammer. Concurrency -- State Models & Java Programs.
Wiley, 1999.
C.A.R. Hoare. Communication Sequential Processes. Prentice Hall, 1986
R. Milner, Communication and Concurrency, Prentice-Hall International,
1989.
M. Reisig, Petri-Nets, Springer-Verlag, Berlin, 1986
E.M. Clarke, B.-H. Schlingloff, Model Checking, in Handbook of
Automated Reasoning, Band II, S. 1637--1790, Elsevier, 2001
D. Harel, M. Politti. Modeling Reactive Systems with Statecharts.
McGraw-Hill
Bernhard
Schätz, 09.11.2005