Symbolic Causality Checking Using Bounded Model Checking

Beer, Adrian; Heidinger, Stephan; Kühne, Uwe; Leitner-Fischer, Florian; Leue, Stefan

Symbolic Causality Checking Using Bounded Model Checking

Files

Beer_294967.pdf(778.84 KB)

Date

2015

Authors

Beer, Adrian

Heidinger, Stephan

Kühne, Uwe

Leitner-Fischer, Florian

Leue, Stefan

Publication type

Preprint

Abstract

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.

Subject (DDC)

004 Computer Science

Cite This

ISO 690

BEER, 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>

Bibliography of Konstanz

Yes