Publikation:

Mining sequential patterns to explain concurrent counterexamples

Lade...
Vorschaubild

Dateien

Leue_243913.pdf
Leue_243913.pdfGröße: 232.3 KBDownloads: 238

Datum

2013

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

BARTOCCI, Ezio, ed., C. R. RAMAKRISHNAN, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 264-281. Lecture Notes in Computer Science. 7976. ISBN 978-3-642-39175-0. Available under: doi: 10.1007/978-3-642-39176-7_17

Zusammenfassung

Concurrent systems are often modeled using an interleaving semantics. Since system designers tend to think sequentially, it is highly probable that they do not foresee some interleavings that their model encompasses. As a consequence, one of the main sources of failure in concurrent systems is unforeseen interleavings. In this paper, we devise an automated method for revealing unforeseen interleavings in the form of sequences of actions derived from counterexamples obtained by explicit state model checking. In order to extract such sequences we use a data mining technique called sequential pattern mining. Our method is based on contrasting the patterns of a set of counterexamples with the patterns of a set of correct traces that do not violate a desired property. We first argue that mining sequential patterns from the dataset of counterexamples fails due to the inherent complexity of the problem. We then propose a reduction technique designed to reduce the length of the execution traces in order to make the problem more tractable. We finally demonstrate the effectiveness of our approach by applying it to a number of sample case studies.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690LEUE, Stefan, Mitra TABAEI BEFROUEI, 2013. Mining sequential patterns to explain concurrent counterexamples. In: BARTOCCI, Ezio, ed., C. R. RAMAKRISHNAN, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 264-281. Lecture Notes in Computer Science. 7976. ISBN 978-3-642-39175-0. Available under: doi: 10.1007/978-3-642-39176-7_17
BibTex
@inproceedings{Leue2013Minin-24391,
  year={2013},
  doi={10.1007/978-3-642-39176-7_17},
  title={Mining sequential patterns to explain concurrent counterexamples},
  number={7976},
  isbn={978-3-642-39175-0},
  publisher={Springer Berlin Heidelberg},
  address={Berlin, Heidelberg},
  series={Lecture Notes in Computer Science},
  booktitle={Model Checking Software},
  pages={264--281},
  editor={Bartocci, Ezio and Ramakrishnan, C. R.},
  author={Leue, Stefan and Tabaei Befrouei, Mitra}
}
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/24391">
    <dc:creator>Tabaei Befrouei, Mitra</dc:creator>
    <dcterms:abstract xml:lang="eng">Concurrent systems are often modeled using an interleaving semantics. Since system designers tend to think sequentially, it is highly probable that they do not foresee some interleavings that their model encompasses. As a consequence, one of the main sources of failure in concurrent systems is unforeseen interleavings. In this paper, we devise an automated method for revealing unforeseen interleavings in the form of sequences of actions derived from counterexamples obtained by explicit state model checking. In order to extract such sequences we use a data mining technique called sequential pattern mining. Our method is based on contrasting the patterns of a set of counterexamples with the patterns of a set of correct traces that do not violate a desired property. We first argue that mining sequential patterns from the dataset of counterexamples fails due to the inherent complexity of the problem. We then propose a reduction technique designed to reduce the length of the execution traces in order to make the problem more tractable. We finally demonstrate the effectiveness of our approach by applying it to a number of sample case studies.</dcterms:abstract>
    <dcterms:issued>2013</dcterms:issued>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-09-12T13:26:28Z</dc:date>
    <dc:language>eng</dc:language>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Tabaei Befrouei, Mitra</dc:contributor>
    <dcterms:bibliographicCitation>Model Checking Software : 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013, Proceedings / Ezio Bartocci ... (eds.). - Berlin : Springer, 2013. - S. 264-281. - (Lecture Notes in Computer Science ; 7976). - ISBN 978-3-642-39175-0</dcterms:bibliographicCitation>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/24391/1/Leue_243913.pdf"/>
    <dc:rights>terms-of-use</dc:rights>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:title>Mining sequential patterns to explain concurrent counterexamples</dcterms:title>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2014-08-30T22:25:06Z</dcterms:available>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/24391"/>
    <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/24391/1/Leue_243913.pdf"/>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen