TY  - THES
AB  - Die vorhandenen Validierungs- und Verifikationstechniken können nicht vollständig sich- erstellen, dass sich die eingebettete Software wirklich wie gewünscht verhält, nachdem sie freigegeben oder eingesetzt wurde. Vor diesem Hintergrund stellen wir einen Online Model Checking Mechanismus vor, um die Korrektheit eines aktuellen Ausführungspfades, anstatt die gesamte Korrektheit der eingebetteten Software, sicherzustellen. Es ist dabei nicht das Ziel, einen schnelleren Model Checking Algorithmus vorzulegen. Die Grundidee des Ansatzes ist es, eine Folge von partiellen Modellen, die den aktuellen Ausführungspfad der zu überprüfenden Software überdecken, während der Systemausführung zu überprüfen. Die Fehler, die in den partiellen Modellen erkannt werden, können mögliche Fehler im Quellcode des zu überprüfenden Systems anzeigen. Die partiellen Modelle entstehen aus dem Verhaltensmodell des zu überprüfenden Systems mittels der aktuellen Zustandsinformation, die während der Laufzeit periodisch aufgenommen wird. Das Online Model Checking Problem reduziert sich zu Online Erreichbarkeitsanalyse, wobei in jedem Überprüfungszyklus nur endlich viele Schritte auf der Modellebene verfolgt werden. Die zu überprüfenden Eigenschaften sind Formeln in Linearer Temporaler Logik. Sowohl Sicherheits- wie auch Lebendigkeitsüberprüfungen lassen sich dabei auf Erreichbarkeitsanalyse während der Laufzeit zurückführen. Mittels Online Model Checking sind wir in der Lage, die Zustände, die sich beliebig tief in dem Zustandsraum befinden, zu erreichen. Dazu können wir auch potenzielle Fehler vorhersagen, selbst wenn der Checking Prozess hinter der Ausführung des zu überprüfenden Systems zurückfällt.
AU  - Zhao, Yuhong
CY  - Paderborn
DP  - Universität Paderborn
LA  - eng
N1  - Tag der Verteidigung: 31.08.2015
N1  - Faculty of Electrical Engineering, Computer Science and Mathematics, University of Paderborn, Univ., Dissertation, 2015
PB  - Veröffentlichungen der Universität
SP  - 1 Online-Ressource (xii, 160 Seiten)
T2  - Institut für Informatik
TI  - Online model checking mechanism and its applications
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:466:2-24091
Y2  - 2026-02-01T03:36:36
ER  -