Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation

Lade...
Vorschaubild
Dateien
12845.pdf
12845.pdfGröße: 640.82 KBDownloads: 323
Datum
2010
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
DiRePro: Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. New York, New York, USA: ACM Press, 2010, pp. 25-32. ISBN 978-1-60558-972-5. Available under: doi: 10.1145/1808877.1808883
Zusammenfassung

The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Algorithms, Reliability, Verification
Konferenz
The 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10, 3. Mai 2010 - 3. Mai 2010, Cape Town, South Africa
Rezension
undefined / . - undefined, undefined
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Datensätze
Zitieren
ISO 690ALJAZZAR, Husain, Matthias KUNTZ, Florian LEITNER-FISCHER, Stefan LEUE, 2010. Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation. The 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. Cape Town, South Africa, 3. Mai 2010 - 3. Mai 2010. In: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. New York, New York, USA: ACM Press, 2010, pp. 25-32. ISBN 978-1-60558-972-5. Available under: doi: 10.1145/1808877.1808883
BibTex
@inproceedings{Aljazzar2010Direc-6116,
  year={2010},
  doi={10.1145/1808877.1808883},
  title={Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation},
  isbn={978-1-60558-972-5},
  publisher={ACM Press},
  address={New York, New York, USA},
  booktitle={Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10},
  pages={25--32},
  author={Aljazzar, Husain and Kuntz, Matthias and Leitner-Fischer, Florian and Leue, Stefan}
}
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/6116">
    <dc:format>application/pdf</dc:format>
    <dcterms:bibliographicCitation>First publ. in: QUOVADIS '10 : Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems May 3, 2010, Cape Town, South Africa / Carlo Ghezzi. New York, NY : ACM, 2010. pp. 25-32</dcterms:bibliographicCitation>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:abstract xml:lang="eng">The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.</dcterms:abstract>
    <dc:contributor>Kuntz, Matthias</dc:contributor>
    <dcterms:issued>2010</dcterms:issued>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:38Z</dc:date>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6116"/>
    <dcterms:title>Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation</dcterms:title>
    <dc:language>eng</dc:language>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6116/1/12845.pdf"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Kuntz, Matthias</dc:creator>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6116/1/12845.pdf"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Aljazzar, Husain</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:38Z</dcterms:available>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:creator>Aljazzar, Husain</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </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
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen