- Aktuell

- Suche

- Kontakt

Seminar Systemmodellierung und Verifikation WS 2007/08

Dozent(in): Dr. Frank Ortmeier, Matthias Güdemann
Termin: Blockseminar am 13.12.
Gebäude/Raum: 2004 L1
Ansprechpartner: Matthias Güdemann
Inhalt: Zustandsbasierte, reaktive, eingebettete Systeme (z. B. Software in Automobilen, Zugsteuerungen, Steuerungen für Lifte und Kopierer u. v. m.) können sehr anschaulich als Automaten modelliert werden. Eine Modellierung als Automat erlaubt die Analyse und Verifikation des Systems in sehr frühen Entwicklungsstadien. Dazu werden insbesondere automatische Verifikationstechniken (z. B. Modelchecking) vermehrt in der Industrie eingesetzt. So ist beispielsweise für die Entwicklung von Hardware Modelchecking mittlerweile ein fester Bestandteil des Entwurfszyklus.

In diesem Seminar werden Themen rund um Automatenmodellierung, Temporallogik und automatischer Verifikation (mit Schwerpunkt Model Checking) aufgegriffen und bearbeitet.

Wichtig:

  • Ameldung bei STUDIS: vom 3.01.2008 (00.01 Uhr) - 15.01.2008 (23.59 Uhr)
    Ohne Anmeldung bei STUDIS können keine Leistungspunkte vergeben werden!

  • Fügen Sie diese Erklärung zu Ihrer Ausarbeitung hinzu, die Sie auf einem Exemplar für Ihren Semararbeitsbetreuer eigenhändig unterschreiben.

Anforderungen:

  • selbständige Erarbeitung der vorgegebenen Literatur
  • Ausarbeitung und Halten eines Vortrags/einer Präsentation (ca. 45 Minuten).
  • schriftliche Ausarbeitung/Bericht (ca. 15 Seiten), die zum Vortrag fertig ist.
  • aktive Teilnahme an den Vorträgen der anderen Teilnehmer.

Themen:

Thema Bearbeiter Betreuer
Sicherheitsanalyse in FSAP / NuSMV-SA Matthias Kus Matthias Güdemann
SCADE: Lustre Baocheng Wang Matthias Güdemann
SCADE: konservative Spracherweiterung mit Automaten Dominik Bösl Matthias Güdemann
Modellierung in TopCased / SysML Jan-Philipp Steghöfer Frank Ortmeier
Sicherheitsanalyse mit Altarica Andreas Luksch Frank Ortmeier
Probabilistisches Modelchecking mit PRISM Martin Burkhardt Frank Ortmeier
Modelchecking von Verilog in SMV Ferry Hielscher Simon Bäumler
Kompositionales Modelchecking in SMV Deniz Hadi Simon Bäumler
CTL Modelchecking Attila Balkan Florian Nafz

   

Zeitplan:

Zeit Thema 
8:00 - 8:45
 
CTL Modelchecking
 
8:50 - 9:35
 
Modelchecking von Verilog in SMV
 
9:40 - 10:25
 
Sicherheitsanalyse in FSAP / NuSMV-SA
 
10:30 - 11:15
 
Probabilistisches Modelchecking mit PRISM
 
12:30 - 13:15
 
SCADE: LUSTRE - Syntax und Semantik
 
13:20 - 14:05
 
SCADE: konservative Spracherweiterung mit Automaten
 
14:10 - 14:55
 
Modellierung in TopCased / SysML
 
15:00 - 15:45
 
Sicherheitsanalyse mit Altarica

 

Ablauf:

  • 1. Schritt: Vorbesprechung am 16.10.2007 um 14.00 Uhr in Raum 2004 L1.
  • 2. Schritt: Erste Themenbesprechung mit dem Betreuer bis zum 24.10.2007.Der Betreuer erläutert genauer das Thema, gibt Tipps zur Literaturrecherche und klärt das weitere Vorgehen.
  • 3. Schritt: Recherche, Ausarbeitung einer Gliederung und Absprache mit dem Betreuer bis zum 12.11.2007 (rechtzeitige Terminvereinbarung!)
  • 4. Schritt: Erstellen Vortrag/Bericht in einer ersten Version bis zum 26.11.2007 und Feedbackbesprechung dazu mit dem Betreuer (rechtzeitige Terminvereinbarung!)
  • 5. Schritt: Endversion Vortrag/Bericht Abgabe bis spätestens zum 07.12.2007
  • 7. Schritt: Vortrag am 13.12.2007

Ansprechpartner:

Anmeldung:

Die Anmeldung zum Seminar findet vom 01.10.2007 - 15.10.2007 per Email statt. Zur Anmeldung müssen 3 Themen (mit jeweiliger Präferenz) angegeben werden. Die genauen Themen werden bis dahin noch bekannt gegeben. 

weitere Informationen zu der Lehrveranstaltung:

empfohlenes Studiensemester der Lehrveranstaltung: Hauptstudium
Fachrichtung Lehrveranstaltung: Informatik
Nummer der Lehrveranstaltung: 07088
Dauer der Lehrveranstaltung: 2 SWS
Typ der Lehrveranstaltung: S - Seminar
Leistungspunkte: 4 LP
Bereich: Theoretische Informatik, Softwaretechnik und Programmiersprachen
Prüfung: Hausarbeit
Semester: WS 2007/08