Clock Bound Repair for Timed Systems

Cite This

Files in this item

Checksum: MD5:ebd4d31443dfe477891208730c6175ca

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, Jul 15, 2019 - Jul 18, 2019. In: DILLIG, Isil, ed., Serdar TASIRAN, ed.. Computer Aided Verification : 31st International Conference, CAV 2019, Proceedings, Part I. Cham:Springer International Publishing, pp. 79-96. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-25539-8. Available under: doi: 10.1007/978-3-030-25540-4_5

@inproceedings{Kolbl2019-07-12Clock-46448, title={Clock Bound Repair for Timed Systems}, year={2019}, doi={10.1007/978-3-030-25540-4_5}, number={11561}, isbn={978-3-030-25539-8}, issn={0302-9743}, address={Cham}, publisher={Springer International Publishing}, 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 xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <bibo:uri rdf:resource=""/> <dcterms:rights rdf:resource=""/> <dspace:hasBitstream rdf:resource=""/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:hasPart rdf:resource=""/> <dcterms:title>Clock Bound Repair for Timed Systems</dcterms:title> <dc:contributor>Wies, Thomas</dc:contributor> <dc:contributor>Kölbl, Martin</dc:contributor> <dspace:isPartOfCollection rdf:resource=""/> <dc:creator>Kölbl, Martin</dc:creator> <dcterms:available rdf:datatype="">2019-07-18T11:05:46Z</dcterms:available> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:language>eng</dc:language> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:issued>2019-07-12</dcterms:issued> <dc:creator>Wies, Thomas</dc:creator> <dcterms:isPartOf rdf:resource=""/> <dc:date rdf:datatype="">2019-07-18T11:05:46Z</dc:date> <dc:rights>terms-of-use</dc:rights> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <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> </rdf:Description> </rdf:RDF>

Downloads since Jul 18, 2019 (Information about access statistics)

Koelbl_2-lr7idu9ozjpr2.pdf 209

This item appears in the following Collection(s)

Search KOPS


My Account