TarTar : A Timed Automata Repair Tool

Lade...
Vorschaubild
Dateien
Koelbl_2-1wnkg9vtbpcez0.pdf
Koelbl_2-1wnkg9vtbpcez0.pdfGröße: 801.87 KBDownloads: 241
Datum
2020
Autor:innen
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
ArXiv-ID
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Bookpart
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
LAHIRI, Shuvendu K., ed., Chao WANG, ed.. Computer Aided Verification : 32nd International Conference, CAV 2020, Proceedings, Part I. Cham: Springer International Publishing, 2020, pp. 529-540. Lecture Notes in Computer Science. 12224. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-53287-1. Available under: doi: 10.1007/978-3-030-53288-8_25
Zusammenfassung

We present TarTar, an automatic repair analysis tool that, given a timed diagnostic trace (TDT) obtained during the model checking of a timed automaton model, suggests possible syntactic repairs of the analyzed model. The suggested repairs include modified values for clock bounds in location invariants and transition guards, adding or removing clock resets, etc. The proposed repairs guarantee that the given TDT is no longer feasible in the repaired model, while preserving the overall functional behavior of the system. We give insights into the design and architecture of TarTar, and show that it can successfully repair 69% of the seeded errors in system models taken from a diverse suite of case studies.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
CAV: International Conference on Computer Aided Verification : 32nd International Conference, 21. Juli 2020 - 24. Juli 2020, Los Angeles, CA
Rezension
undefined / . - undefined, undefined
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Datensätze
Zitieren
ISO 690KÖLBL, Martin, Stefan LEUE, Thomas WIES, 2020. TarTar : A Timed Automata Repair Tool. CAV: International Conference on Computer Aided Verification : 32nd International Conference. Los Angeles, CA, 21. Juli 2020 - 24. Juli 2020. In: LAHIRI, Shuvendu K., ed., Chao WANG, ed.. Computer Aided Verification : 32nd International Conference, CAV 2020, Proceedings, Part I. Cham: Springer International Publishing, 2020, pp. 529-540. Lecture Notes in Computer Science. 12224. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-53287-1. Available under: doi: 10.1007/978-3-030-53288-8_25
BibTex
@inproceedings{Kolbl2020-07-14TarTa-53471,
  year={2020},
  doi={10.1007/978-3-030-53288-8_25},
  title={TarTar : A Timed Automata Repair Tool},
  number={12224},
  isbn={978-3-030-53287-1},
  issn={0302-9743},
  publisher={Springer International Publishing},
  address={Cham},
  series={Lecture Notes in Computer Science},
  booktitle={Computer Aided Verification : 32nd International Conference, CAV 2020, Proceedings, Part I},
  pages={529--540},
  editor={Lahiri, Shuvendu K. and Wang, Chao},
  author={Kölbl, Martin and Leue, Stefan and Wies, Thomas}
}
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/53471">
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-04-23T11:18:10Z</dcterms:available>
    <dcterms:issued>2020-07-14</dcterms:issued>
    <dcterms:abstract xml:lang="eng">We present TarTar, an automatic repair analysis tool that, given a timed diagnostic trace (TDT) obtained during the model checking of a timed automaton model, suggests possible syntactic repairs of the analyzed model. The suggested repairs include modified values for clock bounds in location invariants and transition guards, adding or removing clock resets, etc. The proposed repairs guarantee that the given TDT is no longer feasible in the repaired model, while preserving the overall functional behavior of the system. We give insights into the design and architecture of TarTar, and show that it can successfully repair 69% of the seeded errors in system models taken from a diverse suite of case studies.</dcterms:abstract>
    <dcterms:title>TarTar : A Timed Automata Repair Tool</dcterms:title>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Wies, Thomas</dc:contributor>
    <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by/4.0/"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:language>eng</dc:language>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/53471/1/Koelbl_2-1wnkg9vtbpcez0.pdf"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/53471"/>
    <dc:rights>Attribution 4.0 International</dc:rights>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Kölbl, Martin</dc:creator>
    <dc:contributor>Kölbl, Martin</dc:contributor>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/53471/1/Koelbl_2-1wnkg9vtbpcez0.pdf"/>
    <dc:creator>Wies, Thomas</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-04-23T11:18:10Z</dc:date>
  </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