Bibliographic Metadata
Bibliographic Metadata
- TitleOnline model checking mechanism and its applications : / by Yuhong Zhao
- Author
- Participants
- Published
- EditionElektronische Ressource
- Description1 Online-Ressource (xii, 160 Seiten) : Illustrationen, Diagramme
- Institutional NoteFaculty of Electrical Engineering, Computer Science and Mathematics, University of Paderborn, Univ., Dissertation, 2015
- AnnotationTag der Verteidigung: 31.08.2015
- Defended on2015-08-31
- LanguageEnglish
- Document TypesDissertation (PhD)
- URN
Links
- Social MediaShare
- Reference
- IIIF
Files
Classification
Zusammenfassung
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.
Abstract
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.
Content
Stats
- The PDF-Document has been downloaded 58 times.
License/Rightsstatement
