Symbolic Causality Checking Using Bounded Model Checking

Zitieren

Dateien zu dieser Ressource

Dateien Größe Format Anzeige

Zu diesem Dokument gibt es keine Dateien.

BEER, Adrian, Stephan HEIDINGER, Uwe KÜHNE, Florian LEITNER-FISCHER, Stefan LEUE, 2015. Symbolic Causality Checking Using Bounded Model Checking. 22nd International Symposium, SPIN 2015. Stellenbosch, 24. Aug 2015 - 26. Aug 2015. In: FISCHER, Bernd, ed. and others. Model Checking Software : 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings. 22nd International Symposium, SPIN 2015. Stellenbosch, 24. Aug 2015 - 26. Aug 2015. Cham:Springer International Publishing, pp. 203-221. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-319-23403-8. Available under: doi: 10.1007/978-3-319-23404-5_14

@inproceedings{Beer2015Symbo-31853, title={Symbolic Causality Checking Using Bounded Model Checking}, year={2015}, doi={10.1007/978-3-319-23404-5_14}, number={9232}, isbn={978-3-319-23403-8}, issn={0302-9743}, address={Cham}, publisher={Springer International Publishing}, series={Lecture Notes in Computer Science}, booktitle={Model Checking Software : 22nd International Symposium, SPIN 2015, Stellenbosch, South Africa, August 24-26, 2015, Proceedings}, pages={203--221}, editor={Fischer, Bernd}, author={Beer, Adrian and Heidinger, Stephan and Kühne, Uwe and Leitner-Fischer, Florian and Leue, Stefan} }

<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/rdf/resource/123456789/31853"> <dcterms:issued>2015</dcterms:issued> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/31853"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-09-29T10:03:13Z</dc:date> <dc:creator>Leue, Stefan</dc:creator> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:creator>Leitner-Fischer, Florian</dc:creator> <dc:contributor>Leue, Stefan</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 efficient 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> <dcterms:title>Symbolic Causality Checking Using Bounded Model Checking</dcterms:title> <dc:creator>Kühne, Uwe</dc:creator> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Heidinger, Stephan</dc:contributor> <dc:contributor>Leitner-Fischer, Florian</dc:contributor> <dc:contributor>Kühne, Uwe</dc:contributor> <dc:language>eng</dc:language> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:creator>Beer, Adrian</dc:creator> <dc:contributor>Beer, Adrian</dc:contributor> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2015-09-29T10:03:13Z</dcterms:available> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>Heidinger, Stephan</dc:creator> </rdf:Description> </rdf:RDF>

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto