Symbolic Causality Checking Using Bounded Model Checking


Dateien zu dieser Ressource

Prüfsumme: MD5:5e96b329e6b7fd7e0df8fea08d1a3902

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. 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="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dcterms:issued>2015</dcterms:issued> <bibo:uri rdf:resource=""/> <dc:date rdf:datatype="">2015-09-29T10:03:13Z</dc:date> <dspace:hasBitstream rdf:resource=""/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:isPartOf rdf:resource=""/> <dcterms:hasPart rdf:resource=""/> <dc:creator>Leitner-Fischer, Florian</dc:creator> <dc:rights>terms-of-use</dc:rights> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:rights rdf:resource=""/> <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=""/> <dc:creator>Beer, Adrian</dc:creator> <dc:contributor>Beer, Adrian</dc:contributor> <dcterms:available rdf:datatype="">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>

Dateiabrufe seit 29.09.2015 (Informationen über die Zugriffsstatistik)

Beer_2-1cqocmbol3jvh3.pdf 1

Das Dokument erscheint in:

KOPS Suche


Mein Benutzerkonto