Clock Bound Repair for Timed Systems

Kölbl, Martin; Leue, Stefan; Wies, Thomas

Clock Bound Repair for Timed Systems

Dateien

Koelbl_2-lr7idu9ozjpr2.pdfGröße: 1018.77 KBDownloads: 311

Datum

2019

Autor:innen

Kölbl, Martin

Leue, Stefan

Wies, Thomas

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

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.

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

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_5

BibTex

@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>

Universitätsbibliographie

Ja