TarTar: A Timed Automata Repair Tool

Martin Kölbl; Stefan Leue; Thomas Wies

doi:10.1007/978-3-030-53288-8_25

TarTar: A Timed Automata Repair Tool

Martin Kölbl, Stefan Leue, Thomas Wies

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English (US)
Title of host publication	Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
Editors	Shuvendu K. Lahiri, Chao Wang
Publisher	Springer
Pages	529-540
Number of pages	12
ISBN (Print)	9783030532871
DOIs	https://doi.org/10.1007/978-3-030-53288-8_25
State	Published - 2020
Event	32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States Duration: Jul 21 2020 → Jul 24 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12224 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	32nd International Conference on Computer Aided Verification, CAV 2020
Country/Territory	United States
City	Los Angeles
Period	7/21/20 → 7/24/20

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-53288-8_25

Cite this

Kölbl, M., Leue, S., & Wies, T. (2020). TarTar: A Timed Automata Repair Tool. In S. K. Lahiri, & C. Wang (Eds.), Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings (pp. 529-540). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12224 LNCS). Springer. https://doi.org/10.1007/978-3-030-53288-8_25

TarTar: A Timed Automata Repair Tool. / Kölbl, Martin; Leue, Stefan; Wies, Thomas.
Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. ed. / Shuvendu K. Lahiri; Chao Wang. Springer, 2020. p. 529-540 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12224 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kölbl, M, Leue, S & Wies, T 2020, TarTar: A Timed Automata Repair Tool. in SK Lahiri & C Wang (eds), Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12224 LNCS, Springer, pp. 529-540, 32nd International Conference on Computer Aided Verification, CAV 2020, Los Angeles, United States, 7/21/20. https://doi.org/10.1007/978-3-030-53288-8_25

Kölbl M, Leue S, Wies T. TarTar: A Timed Automata Repair Tool. In Lahiri SK, Wang C, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. Springer. 2020. p. 529-540. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-53288-8_25

Kölbl, Martin ; Leue, Stefan ; Wies, Thomas. / TarTar : A Timed Automata Repair Tool. Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings. editor / Shuvendu K. Lahiri ; Chao Wang. Springer, 2020. pp. 529-540 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0153db3c11e746aabf02f09367c0ddc2,

title = "TarTar: A Timed Automata Repair Tool",

abstract = "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.",

author = "Martin K{\"o}lbl and Stefan Leue and Thomas Wies",

note = "Publisher Copyright: {\textcopyright} 2020, The Author(s).; 32nd International Conference on Computer Aided Verification, CAV 2020 ; Conference date: 21-07-2020 Through 24-07-2020",

year = "2020",

doi = "10.1007/978-3-030-53288-8_25",

language = "English (US)",

isbn = "9783030532871",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "529--540",

editor = "Lahiri, {Shuvendu K.} and Chao Wang",

booktitle = "Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings",

}

TY - GEN

T1 - TarTar

T2 - 32nd International Conference on Computer Aided Verification, CAV 2020

AU - Kölbl, Martin

AU - Leue, Stefan

AU - Wies, Thomas

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85089225502&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85089225502&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-53288-8_25

DO - 10.1007/978-3-030-53288-8_25

M3 - Conference contribution

AN - SCOPUS:85089225502

SN - 9783030532871

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 529

EP - 540

BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings

A2 - Lahiri, Shuvendu K.

A2 - Wang, Chao

PB - Springer

Y2 - 21 July 2020 through 24 July 2020

ER -

TarTar: A Timed Automata Repair Tool

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this