Publikation: Clock Bound Repair for Timed Systems
Lade...
Dateien
Datum
2019
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
DILLIG, Isil, ed., Serdar TASIRAN, ed.. Computer Aided Verification : 31st International Conference, CAV 2019, Proceedings, Part I. Cham: Springer International Publishing, 2019, pp. 79-96. Lecture Notes in Computer Science. 11561. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-25539-8. Available under: doi: 10.1007/978-3-030-25540-4_5
Zusammenfassung
We present algorithms and techniques for the repair of timed system models, given as networks of timed automata (NTA). The repair is based on an analysis of timed diagnostic traces (TDTs) that are computed by real-time model checking tools, such as UPPAAL, when they detect the violation of a timed safety property. We present an encoding of TDTs in linear real arithmetic and use the MaxSMT capabilities of the SMT solver Z3 to compute possible repairs to clock bound values that minimize the necessary changes to the automaton. We then present an admissibility criterion, called functional equivalence, that assesses whether a proposed repair is admissible in the overall context of the NTA. We have implemented a proof-of-concept tool called TarTar for the repair and admissibility analysis. To illustrate the method, we have considered a number of case studies taken from the literature and automatically injected changes to clock bounds to generate faulty mutations. Our technique is able to compute a feasible repair for 91% of the faults detected by UPPAAL in the generated mutants.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Timed automata, Automated repair, Admissibility of repair, TarTar tool
Konferenz
CAV 2019 : 31st International Conference on Computer Aided Verification, 15. Juli 2019 - 18. Juli 2019, New York City, NY, USA
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
KÖLBL, Martin, Stefan LEUE, Thomas WIES, 2019. Clock Bound Repair for Timed Systems. CAV 2019 : 31st International Conference on Computer Aided Verification. New York City, NY, USA, 15. Juli 2019 - 18. Juli 2019. In: DILLIG, Isil, ed., Serdar TASIRAN, ed.. Computer Aided Verification : 31st International Conference, CAV 2019, Proceedings, Part I. Cham: Springer International Publishing, 2019, pp. 79-96. Lecture Notes in Computer Science. 11561. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-25539-8. Available under: doi: 10.1007/978-3-030-25540-4_5BibTex
@inproceedings{Kolbl2019-07-12Clock-46448,
year={2019},
doi={10.1007/978-3-030-25540-4_5},
title={Clock Bound Repair for Timed Systems},
number={11561},
isbn={978-3-030-25539-8},
issn={0302-9743},
publisher={Springer International Publishing},
address={Cham},
series={Lecture Notes in Computer Science},
booktitle={Computer Aided Verification : 31st International Conference, CAV 2019, Proceedings, Part I},
pages={79--96},
editor={Dillig, Isil and Tasiran, Serdar},
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/46448">
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/46448/1/Koelbl_2-lr7idu9ozjpr2.pdf"/>
<dcterms:title>Clock Bound Repair for Timed Systems</dcterms:title>
<dc:creator>Wies, Thomas</dc:creator>
<dc:language>eng</dc:language>
<dc:rights>terms-of-use</dc:rights>
<dc:creator>Kölbl, Martin</dc:creator>
<dc:contributor>Kölbl, Martin</dc:contributor>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/46448"/>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-07-18T11:05:46Z</dcterms:available>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/46448/1/Koelbl_2-lr7idu9ozjpr2.pdf"/>
<dcterms:issued>2019-07-12</dcterms:issued>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:contributor>Leue, Stefan</dc:contributor>
<dc:creator>Leue, Stefan</dc:creator>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-07-18T11:05:46Z</dc:date>
<dcterms:abstract xml:lang="eng">We present algorithms and techniques for the repair of timed system models, given as networks of timed automata (NTA). The repair is based on an analysis of timed diagnostic traces (TDTs) that are computed by real-time model checking tools, such as UPPAAL, when they detect the violation of a timed safety property. We present an encoding of TDTs in linear real arithmetic and use the MaxSMT capabilities of the SMT solver Z3 to compute possible repairs to clock bound values that minimize the necessary changes to the automaton. We then present an admissibility criterion, called functional equivalence, that assesses whether a proposed repair is admissible in the overall context of the NTA. We have implemented a proof-of-concept tool called TarTar for the repair and admissibility analysis. To illustrate the method, we have considered a number of case studies taken from the literature and automatically injected changes to clock bounds to generate faulty mutations. Our technique is able to compute a feasible repair for 91% of the faults detected by UPPAAL in the generated mutants.</dcterms:abstract>
<dc:contributor>Wies, Thomas</dc:contributor>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
