Design and Analysis of Distributed, Interacting Systems (DIS)

Sommersemester 2013
 

Prof. Joel Greenyer

Vorlesung (2TV + 1Ü), 4 Leistungspunkte

Ort Welfengarten 1, Raum F 128
Termin Donnerstags, 10:00 - 12:00
Beginn 04.04.2013 
Prüfung

mündl. Prüfung, in englisch oder deutsch

Übung

Übungsleiter: Raphael Pham

Donnerstags, 13:00 - 13:45, G323

erster Übungstermin: 11.04.2013

Unterlagen Materialien sind über Stud.IP erhältlich

Lernziele

Die Studenten kennen Methoden für die präzise Modellierung verteilter, interagierender Systeme mit Hilfe von Automaten, anderen formalen Sprachen und präzisen Varianten der UML. Auch kennen sie Methoden für die präzise Spezifikation der von einem System erwarteten Verhaltenseigenschaften mit Hilfe Temporaler Logik. Sie kennen Konzepte und Werkzeuge für die automatische, formale Analyse dieser Eigenschaften durch Model-Checking. Zudem haben die Studenten Kenntnis über einige fortgeschrittene Themen wie den szenariobasierten Entwurf von Interaktionen oder die Modellierung und Analyse von Graphtransformationssystemen.

 

Stoffplan

  1. Entwurfsmethodik und Modellierungstechniken (Anwendungsbeispiele, formale Analysemethoden im Entwicklungsprozess, Fehlerquellen, Automaten, andere formale Sprachen, UML mit präziser Semantik)
  2. Model-Checking (Temporale Logik CTL/LTL, LTL-Model-Checking, CTL-Model-Checking, Symbolisches Model-Checking, Werkzeuge: SPIN, NuSMV)
  3. Fortgeschrittene Themen: Szenariobasierter Entwurf und Analyse, Modellierung und Analyse von Graphtransformationssystemen, Entwurf und Analyse von Real-Time-Systemen

 

 

Educational Objectives:

The students will be acquainted with methods for the precise modeling of distributed, interacting system by means of automata, other formal languages, and precise variants of UML. Moreover, they will be familiar with methods for the precise specification of behavioral properties of a system using temporal logic. The students will know concepts and tools for the automated formal analysis of these properties using model-checking. Furthermore, the students will gain insights in advanced topics like the scenario-based design of interactions and the modeling and analysis of graph-transformation systems.

 

Curriculum

 

  1. Design methodology and modeling techniques (examples, formal analysis techniques in the design process, sources of errors, automata, other formal languages, UML with precise semantics)
  2. Model-checking (temporal logic CTL/LTL, LTL model-checking, CTL model-checking, symbolic model-checking, Tools: SPIN, NuSMV)
  3. Advanced topics: scenario-based design and analysis, modeling and analysis of graph-transformation systems, design and analysis of real-time systems.

Materials

Latex template for submissions of assignments: assignment-template.tex

Tutorial 11 slides, prepared Henshin model

Selected Sample Solutions

Nr Lecture Tutorial Exercise Due date
 1  slides (PDF)      
 2

 slides (PDF)

Uppaal example models (ZIP)

  link, revised version will follow  Assignment1  18.04.2013
 3

 slides (PDF)

LTSA example models (ZIP)

slides, LTSA-examples ThriftShop, Person Assignment 2

28.05.2013 (Sunday), 12pm

 4

 slides (PDF)

slides, LTSA-examples crossing as LTSA, Uppaal model of crossing, Martins Approach

Assignment 3 (PDF)

(latex-source)

(new: latex template for assignment submissions: assignment-template.tex)

Promela Example: light_simple.pml
 

 May 9 2013, 8am

5

slides (PDF)

corrected version 13 July (LTL equiv.)

 

Assignment 4 (PDF)

Promela example: CrossingExampleGotoVariant.pml

May 16 2013, 8am
6 slides (PDF)  

Assignment 5 (PDF)

Promela example: production-cell-one-arm.pml

May 30 2013, 8am
7 slides (PDF)

Tutorial 6 slides and notes(PDF)

corrected version, 10.06.2013, 16:30 p.m. 

Assignment 6 (PDF)

Assignment 6 (tex-source), includes the table

libreoffice-template-drawing-automata (ODF)

 June 13 2013, 8am
8 slides (PDF)

Tutorial 7 slides, corrected last example of iterative, invariant interpretation

corrected version, 14.06.2013, 10:20 a.m. 

 Assignment 7 (PDF)

 June 20 2013, 8am
9 slides (PDF) Tutorial 8 slides  Assignment 8 (PDF)  June 27 2013, 8am
10 slides (PDF) Tutorial 9 slides  Assignment 9 (PDF)  July 4 2013, 8am
11

slides (PDF)

updated on July 4

 Assignment 10 (PDF)  July 11 2013, 8am
12 slides (PDF)  Tutorial 11: ScenarioTools Demo (Download Eclipse Installation, for Windows only, more Information about the tool here) prepared Henshin model,   Assignment 11 (PDF)  July 19 2013, 8am
13 slides (PDF)