Symbolic Causality Checking Using Bounded Model Checking

Lade...
Vorschaubild
Dateien
Beer_294967.pdf
Beer_294967.pdfGröße: 778.84 KBDownloads: 354
Datum
2015
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Preprint
Publikationsstatus
Published
Erschienen in
Zusammenfassung

In precursory work we have developed causality checking, a fault localization method for concurrent system models relying on the Halpern and Pearl counterfactual model of causation that identifies ordered occurrences of system events as being causal for the violation of non-reachability properties. Our first implementation of causality checking relies on explicit-state model checking. In this paper we propose a symbolic implementation of causality checking based on bounded model checking (BMC) and SAT solving. We show that this BMC-based implementation is effcient for large and complex system models. The technique is evaluated on industrial size models and experimentally compared to the existing explicit state causality checking implementation. BMC-based causality checking turns out to be superior to the explicit state variant in terms of runtime and memory consumption for very large system models.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690BEER, Adrian, Stephan HEIDINGER, Uwe KÜHNE, Florian LEITNER-FISCHER, Stefan LEUE, 2015. Symbolic Causality Checking Using Bounded Model Checking
BibTex
@unpublished{Beer2015Symbo-31923,
  year={2015},
  title={Symbolic Causality Checking Using Bounded Model Checking},
  author={Beer, Adrian and Heidinger, Stephan and Kühne, Uwe 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/31923">
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/31923/5/Beer_294967.pdf"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/31923"/>
    <dc:contributor>Beer, Adrian</dc:contributor>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Heidinger, Stephan</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-10-07T10:16:14Z</dc:date>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/31923/5/Beer_294967.pdf"/>
    <dc:contributor>Heidinger, Stephan</dc:contributor>
    <dcterms:issued>2015</dcterms:issued>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-10-07T10:16:14Z</dcterms:available>
    <dcterms:title>Symbolic Causality Checking Using Bounded Model Checking</dcterms:title>
    <dc:creator>Kühne, Uwe</dc:creator>
    <dc:contributor>Kühne, Uwe</dc:contributor>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:abstract xml:lang="eng">In precursory work we have developed causality checking, a fault localization method for concurrent system models relying on the Halpern and Pearl counterfactual model of causation that identifies ordered occurrences of system events as being causal for the violation of non-reachability properties. Our first implementation of causality checking relies on explicit-state model checking. In this paper we propose a symbolic implementation of causality checking based on bounded model checking (BMC) and SAT solving. We show that this BMC-based implementation is effcient for large and complex system models. The technique is evaluated on industrial size models and experimentally compared to the existing explicit state causality checking implementation. BMC-based causality checking turns out to be superior to the explicit state variant in terms of runtime and memory consumption for very large system models.</dcterms:abstract>
    <dc:creator>Beer, Adrian</dc:creator>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:language>eng</dc:language>
  </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