Projektseminar Entwurf sicherer eingebetteter Systeme
Im Projektseminar "Entwurf sicherer eingebetteter Systeme" möchten wir aktuelle Methoden zur Verifikation eingebetteter Systeme in der Praxis anwenden. Als Experimentier-Plattform dienen dabei Simulink und Lego Mindstorms Roboter. Das Projektziel wird es sein, ein sicheres, vernetztes und verteiltes eingebettetes System, bestehend aus mehreren intelligenten Robotern, zu entwickeln. Diese müssen sich durch eine Fabrik bewegen, um unterschiedliche Workstations zu erreichen. Zur Entwicklung der Roboter werden wir Simulink verwenden. Simulink ist eine industrielle Modellierungssprache für eingebettete Systeme. Es bietet direkte Unterstützung der Mindstorms-Hardware und erlaubt es so, diese zu modellieren und zu simulieren. Durch automatische Code-Generierung ist es möglich, den Simulink-Entwurf auf die physischen Mindstorms zu übertragen. Um Sicherheiteigenschaften des Systems zu gewährleisten, soll das Simulink-Modell mithilfe des Tools Simulink2dL formal verifiziert werden. Die Grundidee von Simulink2dL besteht darin, Simulink Modelle in die Differential Dynamic Logic (dL), die Inputsprache des interaktiven Theorembeweisers KeYmaera X, zu transformieren. KeYmaera X ermöglicht es dann, Sicherheitseigenschaften des transformierten Modells zu verifizieren. Da die Projektaufgabe verschiedene Bereiche betrifft (Verifikation, Bau der Roboter, Motorsteuerung und Sensorik, Kommunikation, Suchalgorithmen, ...), lässt sie sich hervorragend im Team lösen - die Studierenden können daher auch wertvolle Erfahrungen zur Teamarbeit und dem Projektmanagement sammeln.
Vorlesung und Vorträge: Di 10:15 - 11:45 (SRZ 203)
Projektmeetings: n.V.
Projektraum: Corrensstr. 1, Raum 015
Teilnahme nur mit vorheriger Anmeldung (Anfang Februar).
Learnweb: https://sso.uni-muenster.de/LearnWeb/learnweb2/course/view.php?id=59063
