Symbolic Causality Checking Using Bounded Model Checking

Cite This

Files in this item

Checksum: MD5:304802755fc28823d2c88541f5b601ff

BEER, Adrian, Stephan HEIDINGER, Uwe KÜHNE, Florian LEITNER-FISCHER, Stefan LEUE, 2015. Symbolic Causality Checking Using Bounded Model Checking

@unpublished{Beer2015Symbo-31923, title={Symbolic Causality Checking Using Bounded Model Checking}, year={2015}, author={Beer, Adrian and Heidinger, Stephan and Kühne, Uwe and Leitner-Fischer, Florian and Leue, Stefan} }

<rdf:RDF xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dc:creator>Leue, Stefan</dc:creator> <dc:contributor>Leue, Stefan</dc:contributor> <dc:creator>Leitner-Fischer, Florian</dc:creator> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Heidinger, Stephan</dc:contributor> <dc:creator>Heidinger, Stephan</dc:creator> <dcterms:hasPart rdf:resource=""/> <dcterms:rights rdf:resource=""/> <dc:rights>terms-of-use</dc:rights> <dcterms:isPartOf rdf:resource=""/> <dspace:hasBitstream rdf:resource=""/> <dc:contributor>Kühne, Uwe</dc:contributor> <dc:contributor>Beer, Adrian</dc:contributor> <dc:date rdf:datatype="">2015-10-07T10:16:14Z</dc:date> <dc:language>eng</dc:language> <dc:creator>Kühne, Uwe</dc:creator> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:available rdf:datatype="">2015-10-07T10:16:14Z</dcterms:available> <bibo:uri rdf:resource=""/> <dcterms:title>Symbolic Causality Checking Using Bounded Model Checking</dcterms:title> <dcterms:issued>2015</dcterms:issued> <dc:contributor>Leitner-Fischer, Florian</dc:contributor> <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> <dspace:isPartOfCollection rdf:resource=""/> </rdf:Description> </rdf:RDF>

Downloads since Oct 7, 2015 (Information about access statistics)

Beer_294967.pdf 311

This item appears in the following Collection(s)

Search KOPS


My Account