(BA) Kopplung formaler Modelle mit realweltlichen Systemen

Betreuer: Tim Gonschorek,Frank Ortmeier
Student: Dominik Hamann
Zeitraum: 01.03.2015 - 14.12.2015

Thesis:

Dominik Hamannn: Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen. Otto-von-Guericke-Universität Magdeburg, 2015.

Bei der Entwicklung sicherheitskritischer Systeme werden häufig modellbasierte Analysemethoden eingesetzt. Damit soll sichergestellt werden, dass zuvor definierte Fehlerzu-stände („Hazards“) nicht auftreten können. Für solche Analysen können Model-Checker genutzt werden. Diese prüfen Anhand eines diskreten System-Modells, ob ein „Hazard“ eintreten kann.

 

Da die meisten Systeme Steuer- oder Regelungsaufgaben beinhalten, werden sie oftmals als Kombination von funktionalem Modell und Umgebungsmodell erstellt. Da eine exakte Darstellung der Umgebung sehr komplex werden kann, stellen die meisten Modelle lediglich eine Abstraktion des realen Systems/der realen Umwelt dar. Dies führt dazu, dass bei der Analyse des abstrahierten Modells bestimmte Fehler unentdeckt bleiben, da diese Güte stark vom erstellten Umgebungsmodell abhängt.

Ein Ansatz, solche Abstraktionseinflüsse bei der formalen Sicherheitsanalyse zu minimieren ist, die funktionalen Modelle vom Umgebungsmodell zu lösen und sie mit der realen oder einer annähernd realen (z.B. einer Simulationsumgebung) zu verbinden.

Ziel der Arbeit ist es, eine Verbindung des Verifikationswerkzeuges VECS und der vom Fraunhofer Institut für Fabrikbetrieb und -automatisierung entwickelten VR-Plattform VDT herzustellen, sodass das funktionale Modell als formales Modell simuliert und Sensorwerte aus und Aktorwerte an die VDT-Plattform übertragen werden. Dazu soll ein Konzept entwickelt werden, welches die Kombination der unterschiedlichen Simulationsumgebungen und Zeitsysteme ermöglicht.

(BA) Kopplung formaler Modelle mit realweltlichen Systemen