TarTar: A Timed Automata Repair Tool

Martin Kölbl, Stefan Leue, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationComputer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
EditorsShuvendu K. Lahiri, Chao Wang
PublisherSpringer
Pages529-540
Number of pages12
ISBN (Print)9783030532871
DOIs
StatePublished - 2020
Event32nd International Conference on Computer Aided Verification, CAV 2020 - Los Angeles, United States
Duration: Jul 21 2020Jul 24 2020

Publication series

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

Conference

Conference32nd International Conference on Computer Aided Verification, CAV 2020
CountryUnited States
CityLos Angeles
Period7/21/207/24/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'TarTar: A Timed Automata Repair Tool'. Together they form a unique fingerprint.

Cite this