Counterexample explanation by anomaly detection


Dateien zu dieser Ressource

Prüfsumme: MD5:95ebed10ed77d39a440b5be350621b79

LEUE, Stefan, Mitra TABAEI BEFROUEI, 2012. Counterexample explanation by anomaly detection. In: DONALDSON, Alastair, ed., David PARKER, ed.. Model Checking Software. Berlin, Heidelberg:Springer Berlin Heidelberg, pp. 24-42. ISBN 978-3-642-31758-3

@inproceedings{Leue2012Count-19932, title={Counterexample explanation by anomaly detection}, year={2012}, doi={10.1007/978-3-642-31759-0_5}, number={7385}, isbn={978-3-642-31758-3}, address={Berlin, Heidelberg}, publisher={Springer Berlin Heidelberg}, series={Lecture Notes in Computer Science}, booktitle={Model Checking Software}, pages={24--42}, editor={Donaldson, Alastair and Parker, David}, author={Leue, Stefan and Tabaei Befrouei, Mitra} }

<rdf:RDF xmlns:rdf="" xmlns:bibo="" xmlns:dc="" xmlns:dcterms="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dcterms:issued>2012</dcterms:issued> <bibo:uri rdf:resource=""/> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:bibliographicCitation>First publ. in: Model Checking Software : 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings / edited by Alastair Donaldson... . - Berlin : Springer, 2012. - pp. 24-42. - (Lecture notes in computer science ; 7385). - ISBN 978-3-642-31758-3</dcterms:bibliographicCitation> <dc:contributor>Tabaei Befrouei, Mitra</dc:contributor> <dcterms:available rdf:datatype="">2013-07-31T22:25:03Z</dcterms:available> <dcterms:rights rdf:resource=""/> <dc:date rdf:datatype="">2012-08-07T08:09:51Z</dc:date> <dcterms:title>Counterexample explanation by anomaly detection</dcterms:title> <dc:language>eng</dc:language> <dc:creator>Leue, Stefan</dc:creator> <dc:creator>Tabaei Befrouei, Mitra</dc:creator> <dcterms:abstract xml:lang="eng">Since counterexamples generated by model checking tools are only symptoms of faults in the model, a significant amount of manual work is required in order to locate the fault that is the root cause for the presence of counterexamples in the model. In this paper, we propose an automated method for explaining counterexamples that are symptoms of the occurrence of deadlocks in concurrent systems. Our method is based on an analysis of a set of counterexamples that can be generated by a model checking tool such as SPIN. By comparing the set of counterexamples with the set of correct traces that never deadlock, a number of sequences of actions are extracted that aid the model designer in locating the cause of the occurrence of a deadlock. We first argue that the obvious approach to extract such sequences which is by sequential pattern mining and by contrasting patterns that are typical for the deadlocking counterexample traces but not typical for non-deadlocking traces, fails due to the inherent complexity of the problem. We then propose to extract substrings of specific length that only occur in the set of counterexamples for explaining the occurrence of deadlocks. We use a number of case studies to show the effectiveness of our approach and to compare it with an alternative approach to the counterexample explanation problem.</dcterms:abstract> <dc:rights>deposit-license</dc:rights> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Leue_199325.pdf 152

Das Dokument erscheint in:

KOPS Suche


Mein Benutzerkonto