PV2 ⊧ TarTarsuggests repairs based on a timed diagnostic trace

Given a timed diagnostic trace (TDT) obtained during model checking a timed automaton model, it suggests possible syntactic repairs of the analyzed model

Application domain/field

• Repair analysis
• Timed diagnostic trace (TDT)
• Timed automata
• Model checking
• Syntactic repair
• Automated repair

Type of tool

Automata repair tool

Expected input

• Uppaal model
• Which kind of repair to compute
• Optional: Timed diagnostic trace of the Uppaal model. If this is not given, TarTar will call Uppaal to compute this.

Expected output

One repaired model file for every computed repair and a text file that summarizes which repairs are admissible.

Internals

Timed diagnostic trace (TDT): A timed counterexample that shows a requirement violation. This can be obtained from a model checker. TarTar can be used for the repair of networks of timed automata (NTA). Uses UPPAAL for model checking and computing TDTs, Z3 for solving partial MaxSMT problems, opaal and LearnLib for checking admissibility of a repair, LTSMin.

Comments

License: MIT