TY  - THES
AB  - Die korrekte Funktionalität rechnergesteuerter Systeme ist von großer Wichtigkeit, da diese Systeme oftmals in sicherheitskritischen Szenarios eingesetzt werden. Viele dieser Systeme besitzen zeitgesteuertes Verhalten. Um die Qualität der Systeme sicherzustellen, können Modell-basierte Design-Ansätze verwendet werden in denen die zu erstellenden Systeme mithilfe von Modellen entworfen werden. Die Nutzung formaler Methoden kann die Abwesenheit von fehlerhaftem Verhalten sicherstellen. In dieser Arbeit werden Netzwerke von zeitlichen Automaten betrachtet. Die Analyse dieser Modelle ist schwierig, insbesondere bei der Exploration großer, komplexer Modelle. Zusätzlich gehen bestehende Analyseverfahren nicht effizient mit Änderungen am Model um. In dieser Arbeit wird eine Technik zur Verifikation von Sicherheitseigenschaften, die die Abwesenheit von fehlerhaftem Verhalten definieren, vorgestellt. Diese Technik hat ein grundlegend anderes Funktionsprinzip als andere Ansätze, da sie Induktion nutzt und versucht die explizite Exploration und Speicherung von Zuständen zu vermeiden. Hierdurch ist sie eine wertvolle Ergänzung zu den bestehenden Ansätzen. Bei Änderungen am Modell werden die errechneten induktiven Invarianten des Ansatzes wiederverwendet. Dies funktioniert sehr gut bei einer speziellen Art von Systemen, genannt Parametrisierte Zeitliche Systeme, in der der Parameter die Anzahl der zeitlichen Automaten vorgibt. Die Technik erlaubt die Verifikation der gesamten Familie an Modellen, unabhängig von der Anzahl an Automaten. Hierzu wird die Sicherheitseigenschaft für die kleineren Modelle verifiziert und danach verwendet, um über die gesamte Familie an Modellen zu urteilen. Zusätzlich wird untersucht, wie man die induktiven Invarianten für allgemeine Änderungen und Modelle nutzen kann.
AU  - Isenberg, Tobias
CY  - Paderborn
DA  - 2016
DP  - Universität Paderborn
LA  - eng
N1  - Tag der Verteidigung: 10.05.2016
N1  - Universität Paderborn, Fakultät für Elektrotechnik, Informatik und Mathematik, Univ., Dissertation, 2016
PB  - Veröffentlichungen der Universität
PY  - 2016
SP  - 1 Online-Ressource (xvi, 203 Seiten)
T2  - Institut für Informatik
TI  - Induction-based Verification of Timed Systems
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:466:2-24641
Y2  - 2025-04-25T13:10:29
ER  -