Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

Modellierung und Analyse eingebetteter und verteilter Systeme

Vorlesung WS 20/21 (4 SWS Vorlesung, Nr. 041213, 2 SWS Übung, Nr.  041214)

Modellierung und Analyse eingebetteter und verteilter Systeme

Zeit:
  • Mo 10:00 - 12:00, Otto-Hahn-Str. 16 - R. 205
  • Do 12:00 - 14.00, Otto-Hahn-Str. 16 - R. 205

Aktuelles:

Aufgrund der aktuellen Situation wird es zur Vorlesung ein Online-Angebot geben. Wie dieses konkret aussehen wird und ob und in welcher Form  es Prasenzangbote geben wird, richtet sich nach der Situation im November/Dezember. Die Vorlesung beginnt in KW 45. Im Oktober werde ich ein Video ins Netz stellen, das eine kurze Übersicht über die Vorlesungsinhalte gibt.

Veranstalter:  
  • Peter Buchholz    (Tel.: (0231) 755 4746, Email: peter.buchholz@cs.tu-dortmund.de),

 

Inhalt der Vorlesung:

Die Vorlesung „Modellgestütze Analyse eingebetteter und verteilter Systeme“ führt in das große Gebiet der modellgestützten Systemanalyse. Dabei geht insbesondere um die Analyse von Systemen zur Steuerung oder Überwachung von physikalischen Prozesse. Man spricht in diesem Fall von cyber-physikalischen Systemen. Da die meisten cyber-physischen Systeme heute verteilt sind, muss in eine Analyse neben der eigentlichen eingebetteten Steuerungssoftware auch die Software zur Kommunikationssteuerung mit einbezogen werden. Die in eingebetteten Systemen verwendeten Softwarekomponenten haben oftmals eine relativ einfache Struktur, müssen aber strikte Anforderungen bzgl. Funktionalität, Leistung und Zuverlässigkeit erfüllen. Um sicherzustellen, dass System die Anforderungen einhält, werden in der Regel modellbasierte Verfahren genutzt.  

Die Vorlesung bietet eine umfassende Einführung in die modellbasierte Analyse ereignisdiskreter Systeme. Systeme werden unter den folgenden Aspekten analysiert:

·        Korrekte Funktionalität

·        Ausreichende Leistung

·        Einhaltung von Zeitschranken

·        Sicherstellung einer ausreichenden Verfügbarkeit und Zuverlässigkeit

In der Literatur werden die verschiedenen Analyseziele oft separat behandelt, obwohl sie ähnlich Methoden und Modelle nutzen. Die Vorlesung bringt die vorhandenen Ansätze in einen gemeinsamen Rahmen und erläutert die Zusammenhänge der Gebiete.

Gliederung

  1.       Einführung (Folien)
  2.       Funktionale Analyse - Modelle und Transitionssysteme ( Folien)
  3.      Systemverhalten und nicht-funktionale Eigenschaften (Folien)
  4.       Messung und Datenrepräsentation (Folien)
  5.       Markov Prozesse und - Modelle (Folien)
  6.       Leistungsanalyse mit Warteschlangennetzen (Folien)
  7.       Funktionale Analyse - Model Checking und Eigenschaftsbeweise (Folien)
  8.       Analyse von Realzeitsystemen und -eigenschaften (Folien)
  9.       Zuverlässigkeitsanalyse und Fehlertoleranzverfahren (Teil 1, Teil 2)

Die Folien zu den einzelnen Kapiteln werden vorlesungsbegleitend zur Verfügung gestellt. Ein Zugriff auf die Folien ist nur aus dem Netz der TU bzw. per VPN möglich. Zurzeit befinden sich noch die Folien aus dem letzten Jahr im Netz. Überabreitete Versionen werden im Lauf des Semesters bereit gestellt.

Literatur

Es gibt kein Lehrbuch, das den Stoff der gesamten Vorlesung abdeckt. Größere Teile der Vorlesung findet man in den folgenden Lehrbüchern.

·        Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press 2008.

·        Christos G. Cassandras, Stéphane Lafortune. Introduction to Discrete Event Systems. 2nd edition, Springer 2008.

·        C. Mani Krishna, Israel Koren. Fault-Tolerant Systems. Morgan Kaufman 2007

·        William J. Stewart. Probability, Markov Chains, Queues, and Simulation. Princeton University Press 2009.

-       Kishor S. Trivedi, Andrea Bobbio. Reliability and Availability Engineering. Cambridge University Press 2017.

Weitere Literaturangaben werden in den einzelnen Kapiteln gegeben.

Weitere Links

Die folgenden Softwarewerkzeuge werden in Teilen der Vorlesung genutzt:

·        Java Modeling Tools 

·        Model Checker Spin

·        Model Checker SMV 

·        Model checker UPPAAL

·        Fault Tree Analyzer

 


 Voraussetzungen

Die Vorlesung setzt Basiskenntnisse aus einem Bachelorstudium der Informatik oder ähnlicher Fachrichtungen voraus. Notwendig sind insbesondere Grundkenntnisse in Rechnernetzen, eingebetteten Systemen sowie Wahrscheinlichkeitsrechnung.

Hilfreich, aber nicht Voraussetzung, sind die Wahlpflichtvorlesungen „Eingebettete Systeme“ und "modellgestützte Analyse und Optimierung“ aus dem Bachelor-Studiengang.