Details

Autor(en) / Beteiligte

• Zhao, Yuhong
• Rammig, Franz Josef[Akademischer Betreuer]
• Glässer, Uwe[Akademischer Betreuer]

Titel

Online model checking mechanism and its applications

Ort / Verlag

Paderborn

Erscheinungsjahr

January 2016

Verknüpfte Titel

Beschreibungen/Notizen

• Tag der Verteidigung: 31.08.2015
• ger: 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.
• eng: The existing validation and verification techniques cannot completely ensure that the embedded software does behave as desired after it is released or deployed. Against this background, we present an online model checking mechanism aimed to ensure the correctness of the actual execution trace, instead of the universal correctness, of the embedded software system. Notice that we dont mean to propose a faster model checking algorithm. The basic idea is to check during system execution a sequence of bounded models that cover the actual execution trace of the software system under investigation. Errors detected in the bounded models may indicate potential errors in the source code of the target system. The bounded models are derived from the behavioral model of the target system using the actual state information monitored periodically during system execution. The online model checking problem is reduced to online reachability analysis, which tries to look ahead finitely many steps on the model level. The properties to be checked are specified in linear temporal logic. Because the checking process is done on the model level, both safety and liveness properties can be handled during runtime. By doing model checking online, we are able to reach those states that locate arbitrarily deep in the state space and to predict potential errors even if the checking process falls behind the execution of the target system.