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

Abstract

Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu überprüfen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gefährdende Situationen zu überprüfen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrif t insbesondere Systeme, die nicht nur rein logische Aufgaben ausführen, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu große Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten würde. Die Ergebnisse eines Model Checkers sind dann für dieses Modell nicht aussagekräftig.

In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden können. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss über die Validität des verwendeten Umgebungsmodells bringen.

BibTeX (Download)

@mastersthesis{BAHamann2015,
title = {Kopplung formaler Modelle mit realweltlichen Umgebungsmodellen},
author = {Dominik Hamannn},
editor = {Otto-von-Guericke-Universit\"{a}t Magdeburg},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2015/12/BAHamann2015.pdf},
year  = {2015},
date = {2015-12-14},
address = {Universit\"{a}tsplatz 2, 39106 Magdeburg},
school = {Otto-von-Guericke-Universit\"{a}t Magdeburg},
abstract = {Sicherheitskritische technische Systeme werden insbesondere in der Automobilindustrie und der Luftfahrt immer komplexer. Ein Ansatz, um die Sicherheit solcher Systeme zu \"{u}berpr\"{u}fen, besteht darin, ein Modell des Systems zu erstellen und dieses von einem Model Checker auf gef\"{a}hrdende Situationen zu \"{u}berpr\"{u}fen. Die Umgebung eines softwareintensiven Systems muss oft, aufgrund der Funktionsweise von Model Checkern und aufgrund von Restriktionen der verwendeten Sprache, mit einem hohen Abstraktionsgrad modelliert werden. Das betrift insbesondere Systeme, die nicht nur rein logische Aufgaben ausf\"{u}hren, sondern mittels Sensorik und Aktorik mit der realen Welt interagieren. Herrscht eine zu gro\sse Diskrepanz zwischen der realen Umgebung und dem Modell der Umgebung, tritt in dem Modell Fehlverhalten nicht auf, dass in der realen Welt auftreten w\"{u}rde. Die Ergebnisse eines Model Checkers sind dann f\"{u}r dieses Modell nicht aussagekr\"{a}ftig.

In dieser Arbeit wird eine Schnittstelle vorgestellt, mit der formale Modelle mit realweltlichen Umgebungsmodellen gekoppelt werden k\"{o}nnen. Dadurch wird getestet, inwiefern sich das Verhalten des formalen Modells in einer realistischen Umgebung von dem Verhalten einer abstrahierten Umgebung unterscheidet. Dieser Vergleich kann Aufschluss \"{u}ber die Validit\"{a}t des verwendeten Umgebungsmodells bringen.},
howpublished = {Bachelorarbeit},
keywords = {co-simulation of system models, model-based verfication},
pubstate = {published},
tppubtype = {mastersthesis}
}