Tim Gonschorek: Methodik zur Abstraktion kontinuierlicher Differentialgleichungen. Otto-von-Guericke-University Magdeburg, 2013.

Abstract

Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle
abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage
einer vorgegebenen Spezi kation automatisiert veri ziert werden. Jedoch konnen
die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein
kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese
Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle
sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird
dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein
konkretes Vorgehen erklart, um kontinuierliche Di erentialgleichungen in Di erenzengleichungen
umzuwandeln, die in Zustandsubergangen eingebunden werden konnen.
Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Veri kation
kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat
das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers
Aussagen tre en zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert.
Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von
einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird
die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in
eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers
gegen eine vorgegebene Spezi kation zu veri zieren. Diese Komponente soll als erste
Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung
dienen.

BibTeX (Download)

@mastersthesis{Gonschorek2013,
title = {Methodik zur Abstraktion kontinuierlicher Differentialgleichungen},
author = {Tim Gonschorek},
editor = {Tim Gonschorek},
url = {https://cse.cs.ovgu.de/cse-wordpress/wp-content/uploads/2017/10/BA_2013_Gonschorek.pdf},
year  = {2013},
date = {2013-06-19},
address = {Universit\"{a}tsplatz 2, 39106 Magdeburg},
school = {Otto-von-Guericke-University Magdeburg},
abstract = {Reale Phanomene aus Natur und Technik konnen oft nur durch kontinuierliche Modelle
abgebildet werden. Mithilfe eines Modelchecker konnen Modelle auf Grundlage
einer vorgegebenen Spezikation automatisiert veriziert werden. Jedoch konnen
die meisten Modelchecker nur mit diskreten Modellen umgehen. Deshalb kann ein
kontinuierliches Modell nicht direkt mit einem Modelchecker gepruft werden. Diese
Arbeit prasentiert eine Methodik, mit der es moglich ist, kontinuierliche Modelle
sowohl im Zeitbereich, als auch im Wertebereich zu diskretisieren. Das Modell wird
dazu in einen endlichen, diskreten Zustandsautomaten umgewandelt. Es wird ein
konkretes Vorgehen erklart, um kontinuierliche Dierentialgleichungen in Dierenzengleichungen
umzuwandeln, die in Zustandsubergangen eingebunden werden konnen.
Dadurch wird es moglich, die Vorteile eins Modelcheckers fur die Verikation
kontinuierlicher Modelle zu nutzen. Um sicherzustellen, dass der erstellte Automat
das kontinuierliche Modell hinreichend abstrahiert, um mithilfe eines Modelcheckers
Aussagen treen zu konnen, wird die Methodik anhand eines Beispielmodells evaluiert.
Um die praktische Anwendbarkeit zu zeigen, wird ein komplexe Fallstudie von
einem Modelica-Modell in einen SAML-Automaten transformiert. DesWeiteren wird
die Architektur einer Java-Komponente vorgestellt, mit der eine Modelica-Datei in
eine SAML-Datei transformiert werden kann, um sie mithilfe eines Modelcheckers
gegen eine vorgegebene Spezikation zu verizieren. Diese Komponente soll als erste
Implementation eines Importers fur Modelica-Dateien in eine SAML Umgebung
dienen.},
keywords = {hybrid model checking, model based verification},
pubstate = {published},
tppubtype = {mastersthesis}
}