Directed Diagnostics of System Dependability Models

Lade...
Vorschaubild
Dateien
HusainAljazzar_Diss_toPublish.pdf
HusainAljazzar_Diss_toPublish.pdfGröße: 4.06 MBDownloads: 1250
Datum
2009
Autor:innen
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
EU-Projektnummer
DFG-Projektnummer
Angaben zur Forschungsförderung (Freitext)
Projekt
Open Access-Veröffentlichung
Gesperrt bis
Titel in einer weiteren Sprache
Gerichtete Diagnostik von Systemverlässlichkeitsmodellen
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Dissertation
Publikationsstatus
Published
Erschienen in
Zusammenfassung

Model-Checking ist ein formales Verifikationsverfahren, in dem das Hauptziel die Überprüfung der Korrektheit von Systemen bezüglich gegebener Anforderungen ist. Daneben wird Model-Checking häufig als ein Debugging-Werkzeug eingesetzt. Es wird zur Lokalisierung und Behebung von Fehlern verwendet, wenn das Modell eine gewünschte Eigenschaft verletzt. Aus diesem Grund ist die Möglichkeit, diagnostische Informationen zu liefern, entscheidend für die praktische Anwendbarkeit von Model-Checking-Techniken. Gegenbeispiele sind ein wichtiger Vertreter für solche diagnostische Informationen. Ein Gegenbeispiel besteht in der Regel aus Informationen über das Systemverhalten, welche die Eigenschaftsverletzung belegen und bei der Bestimmung der Ursache dieser Verletzung helfen.
Stochastisches Model-Checking erweitert das konventionelle Model-Checking um die Verifikation quantitativer Leistungs- und Verlässlichkeitsanforderungen. Der Kern des stochastischen Model-Checking besteht aus einer Reihe numerischer Algorithmen. Diese Algorithmen berechnen die Wahrscheinlichkeitswerte, die über die Erfüllung der zu überprüfenden Anforderungen entscheiden. Aufgrund der numerischen Natur dieser Algorithmen liefern stochastische Model-Checker keine Gegenbeispiele. Diese Dissertation präsentiert unsere Forschung zur Lösung dieses Problems. Im Rahmen dieser Forschung ist es uns als erste gelungen, stochastisches Model-Checking um die Generierung und Analyse von Gegenbeispielen zu erweitern. Wir haben das Konzept der Gegenbeispiele in das stochastische Model-Checking eingeführt und die ersten Methoden zur Generierung und Analyse von Gegenbeispielen entwickelt.
Wir beginnen diese Dissertation mit einer Einführung in das stochastische Model-Checking. Danach behandeln wir das Konzept von Gegenbeispielen in diesem Zusammenhang. Wir geben eine formale Definition von Gegenbeispielen bezüglich gängiger stochastischer Modelle. Wir diskutieren anschließend die Aussagefähigkeit von Gegenbeispielen bezüglich Debugging und erläutern die Kriterien von aussagefähigen Gegenbeispielen. Danach präsentieren wir eine Reihe von neuen Methoden zur Generierung von informativen Gegenbeispielen. Unsere Methoden basieren auf heuristischen, oder auch gerichteten, Suchalgorithmen. Wir untersuchen diese Methoden unter verschiedenen Bedingungen und betrachten deren Vor- und Nachteile. Wir untersuchen deren Anwendbarkeit in der Praxis für Modelle mit hoher Komplexität. Wir demonstrieren die Effizienz und Skalierbarkeit unserer Methoden anhand von ausführlichen Experimenten mit realistischen Fallstudien. Diese Experimente zeigen auch, dass die erzeugten Gegenbeispiele informativ und nützlich bei der Fehlerbehebung sind.
Wie wir in dieser Dissertation zeigen werden, sind Gegenbeispiele im stochastischen Model-Checking in der Regel sehr komplex. Infolgedessen stellt die Analyse solcher Gegenbeispiele zu Debugging-Zwecken eine große Herausforderung für die Benutzer dar. Wir haben eine Methode zur Unterstützung des Benutzers bei der Analyse von Gegenbeispielen entwickelt. Diese Methode setzt interaktive Visualisierungstechniken ein, um kausale Faktoren, die die Eigenschaftsverletzung verursacht haben, zu bestimmen.
Ein wichtiger Beitrag unserer Forschung ist die Entwicklung eines neuen gerichteten Suchalgorithmus K* zur Lösung des Problems der k-kürzesten-Pfade. Das Problem der k-kürzesten-Pfade ist ein allgemeines Problem mit vielen Anwendungsgebieten. Dabei handelt es sich um das Finden der k kürzesten Pfade von einem Start- zu einem Zielknoten in einem gerichteten Graphen, wobei k eine beliebige natürliche Zahl ist. Im Gegensatz zu existierenden Algorithmen ist K* auch auf sehr große und komplexe Graphen effizient anwendbar. Wir demonstrieren die Überlegenheit von K mit Hilfe von Experimenten im Bereich der Routenplanung im Straßennetz der USA.

Zusammenfassung in einer weiteren Sprache

Model checking, as a formal verification technique, aims primarily at proving the correctness of systems. Nevertheless, model checking has also been extensively used as a debugging technique to aid developers in locating and fixing errors when the model violates a desired property. Thus, the ability to provide diagnostic information, that facilitates debugging, dictates the usability of model checking techniques in practice. Counterexamples are the prime example of such diagnostic information. A counterexample is in general a piece of information which attests the property violation and which can be used for explaining the causal factors of the property violation.
Stochastic model checking extends conventional model checking with the verification of quantitative performance and dependability requirements. The core of stochastic model checkers is a set of efficient numerical algorithms which compute the probabilities that determine the satisfaction or violation of a given property. Due to the numerical nature of these algorithms, stochastic model checkers do not provide counterexamples. Within our research in this field we succeeded in extending stochastic model checking to include the possibility of counterexample generation. We introduced the notion of counterexamples into stochastic model checking and devised the first methods for the generation and analysis of counterexamples.
We begin this dissertation with an introduction into stochastic model checking followed by a study of counterexamples in stochastic model checking where we give a formal definition for counterexamples for common stochastic models. We also discuss the characteristics of informative counterexamples in this context and present a variety of novel methods for the generation of informative counterexamples. Our methods are based on heuristics-guided search algorithms, also called directed search algorithms. We investigate these methods in different settings and examine their advantages and disadvantages. We also investigate their applicability to models with real-life complexity. We present extensive experiments using significant case studies. These experiments demonstrate the efficiency and scalability of our methods. They also show that the counterexamples produced by our methods are informative and useful for debugging.
Counterexamples in stochastic model checking, as we will show in this dissertation, are very complex. Thus, analysing them for the purpose of debugging is a very challenging task for human users. We propose the first method which aids engineers in analysing counterexample in stochastic model checking. Our method employs interactive visualisation techniques which aim at determining the causal factors of property violations.
A significant contribution of our research on counterexample generation is the development of a novel directed search algorithm K* for solving the k-shortest-paths problem. This is the problem of finding k shortest paths form a start to a target node in a weighted directed graph for an arbitrary natural number k. The k-shortest-paths problem is a general problem with a wide range of applications. K* scales to very large graphs compared to classical k-shortest-paths algorithms. We demonstrate the advantage of K* by applying it to route planning in the US road map.

Fachgebiet (DDC)
004 Informatik
Schlagwörter
Heuristische Suche, Directed Search, Stochastisches Model Checking, Gegenbeispiele, Analyse von Gegenbeispielen, Visualisierung von Gegenbeispielen, Heuristic Search, Stochastic Model Checking, Counterexamples, K-Shortest-Paths, Counterexample Visualisation, Counterexample Analysis
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690ALJAZZAR, Husain, 2009. Directed Diagnostics of System Dependability Models [Dissertation]. Konstanz: University of Konstanz
BibTex
@phdthesis{Aljazzar2009Direc-5887,
  year={2009},
  title={Directed Diagnostics of System Dependability Models},
  author={Aljazzar, Husain},
  address={Konstanz},
  school={Universität Konstanz}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/5887">
    <dcterms:alternative>Gerichtete Diagnostik von Systemverlässlichkeitsmodellen</dcterms:alternative>
    <dc:language>eng</dc:language>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:format>application/pdf</dc:format>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:issued>2009</dcterms:issued>
    <dc:creator>Aljazzar, Husain</dc:creator>
    <dcterms:title>Directed Diagnostics of System Dependability Models</dcterms:title>
    <dcterms:abstract xml:lang="deu">Model-Checking ist ein formales Verifikationsverfahren, in dem das Hauptziel die Überprüfung der Korrektheit von Systemen bezüglich gegebener Anforderungen ist. Daneben wird Model-Checking häufig als ein Debugging-Werkzeug eingesetzt. Es wird zur Lokalisierung und Behebung von Fehlern verwendet, wenn das Modell eine gewünschte Eigenschaft verletzt. Aus diesem Grund ist die Möglichkeit, diagnostische Informationen zu liefern, entscheidend für die praktische Anwendbarkeit von Model-Checking-Techniken. Gegenbeispiele sind ein wichtiger Vertreter für solche diagnostische Informationen. Ein Gegenbeispiel besteht in der Regel aus Informationen über das Systemverhalten, welche die Eigenschaftsverletzung belegen und bei der Bestimmung der Ursache dieser Verletzung helfen.&lt;br /&gt;Stochastisches Model-Checking erweitert das konventionelle Model-Checking um die Verifikation quantitativer Leistungs- und Verlässlichkeitsanforderungen. Der Kern des stochastischen Model-Checking besteht aus einer Reihe numerischer Algorithmen. Diese Algorithmen berechnen die Wahrscheinlichkeitswerte, die  über die Erfüllung der zu  überprüfenden Anforderungen entscheiden. Aufgrund der numerischen Natur dieser Algorithmen liefern stochastische Model-Checker keine Gegenbeispiele. Diese Dissertation präsentiert unsere Forschung zur Lösung dieses Problems. Im Rahmen dieser Forschung ist es uns als erste gelungen, stochastisches Model-Checking um die Generierung und Analyse von Gegenbeispielen zu erweitern. Wir haben das Konzept der Gegenbeispiele in das stochastische Model-Checking eingeführt und die ersten Methoden zur Generierung und Analyse von Gegenbeispielen entwickelt.&lt;br /&gt;Wir beginnen diese Dissertation mit einer Einführung in das stochastische Model-Checking. Danach behandeln wir das Konzept von Gegenbeispielen in diesem Zusammenhang. Wir geben eine formale Definition von Gegenbeispielen bezüglich gängiger stochastischer Modelle. Wir diskutieren anschließend die Aussagefähigkeit von Gegenbeispielen bezüglich Debugging und erläutern die Kriterien von aussagefähigen Gegenbeispielen. Danach präsentieren wir eine Reihe von neuen Methoden zur Generierung von informativen Gegenbeispielen. Unsere Methoden basieren auf heuristischen, oder auch gerichteten, Suchalgorithmen. Wir untersuchen diese Methoden unter verschiedenen Bedingungen und betrachten deren Vor- und Nachteile. Wir untersuchen deren Anwendbarkeit in der Praxis für Modelle mit hoher Komplexität. Wir demonstrieren die Effizienz und Skalierbarkeit unserer Methoden anhand von ausführlichen Experimenten mit realistischen Fallstudien. Diese Experimente zeigen auch, dass die erzeugten Gegenbeispiele informativ und nützlich bei der Fehlerbehebung sind.&lt;br /&gt;Wie wir in dieser Dissertation zeigen werden, sind Gegenbeispiele im stochastischen Model-Checking in der Regel sehr komplex. Infolgedessen stellt die Analyse solcher Gegenbeispiele zu Debugging-Zwecken eine große Herausforderung für die Benutzer dar. Wir haben eine Methode zur Unterstützung des Benutzers bei der  Analyse von Gegenbeispielen entwickelt. Diese Methode setzt interaktive Visualisierungstechniken ein, um kausale Faktoren, die die Eigenschaftsverletzung verursacht haben, zu bestimmen.&lt;br /&gt;Ein wichtiger Beitrag unserer Forschung ist die Entwicklung eines neuen gerichteten Suchalgorithmus K* zur Lösung des Problems der k-kürzesten-Pfade. Das Problem der k-kürzesten-Pfade ist ein allgemeines Problem mit vielen Anwendungsgebieten. Dabei handelt es sich um das Finden der k kürzesten Pfade von einem Start- zu einem Zielknoten in einem gerichteten Graphen, wobei k eine beliebige natürliche Zahl ist. Im Gegensatz zu existierenden Algorithmen ist K* auch auf sehr große und komplexe Graphen effizient anwendbar. Wir demonstrieren die Überlegenheit von K  mit Hilfe von Experimenten im Bereich der Routenplanung im Straßennetz der USA.</dcterms:abstract>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5887"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Aljazzar, Husain</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5887/1/HusainAljazzar_Diss_toPublish.pdf"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5887/1/HusainAljazzar_Diss_toPublish.pdf"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:01:03Z</dc:date>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:01:03Z</dcterms:available>
    <dc:rights>terms-of-use</dc:rights>
  </rdf:Description>
</rdf:RDF>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
November 3, 2009
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Begutachtet
Diese Publikation teilen