Clock Bound Repair for Timed Systems

Martin Kölbl, Stefan Leue, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 31st International Conference, CAV 2019, Proceedings
EditorsIsil Dillig, Serdar Tasiran
PublisherSpringer Verlag
Pages79-96
Number of pages18
ISBN (Print)9783030255398
DOIs
StatePublished - 2019
Event31st International Conference on Computer Aided Verification, CAV 2019 - New York City, United States
Duration: Jul 15 2019Jul 18 2019

Publication series

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

Conference

Conference31st International Conference on Computer Aided Verification, CAV 2019
Country/TerritoryUnited States
CityNew York City
Period7/15/197/18/19

Keywords

  • Admissibility of repair
  • Automated repair
  • TarTar tool
  • Timed automata

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Clock Bound Repair for Timed Systems'. Together they form a unique fingerprint.

Cite this