# TChecker

TChecker is a model-checking tool for real-timed systems developped at LaBRI by Frédéric Herbreteau, Gerald Point and Thanh-Tung Tran.

## Features

TChecker has been designed as a platform for the experimentation of verification algorithms for real-time systems. It provides a collection of libraries (data structures, algorithms, etc.) to ease the implementation of verification algorithms. Systems are modeled as a network of timed automata with synchronous and asynchronous actions, discrete variables over finite domains and dense-time clocks. Supported inputs include UPPAAL bytecode (version 4.0.X) and C++ (using TChecker libraries).

Specifications are written directly in the model as an observer. Model-checking is thus reduced to the emptiness problem for timed automata. TChecker implements emptiness and Büchi emptiness algorithms. Emptiness algorithms feature UPPAAL-like algorithm and dynamic bound algorithms using non-convex abstractions[2,4,5]. Algorithms for Büchi emptiness include Couvreur's algorithm combined with Strongly non-Zeno construction, and guessing zone graph based algorithms[1,3,6,7,8].

As an experimentation platform, TChecker does not only outputs an answer to an emptiness query but various statistics, as well as zone graphs, reachable states and spanning trees computed by the various algorithms.

## Download

### TChecker

First release coming soon

### Benchmarks

We use the following models for our benchmark. Models are given in UPPAAL XML format. See also UPPAAL benchmarks webpage, MCMT benchmarks webpage and PAT benchmarks webpage.

- Critical region [critical-region5.xml]
- Source: PAT benchmarks
- Our model has 5 processes. Bigger or smaller instances are obtained by modifying the value of constant N.
- CSMA/CD protocol [csma-cd9.xml]
- Source: S. Tripakis and S. Yovine. Analysis of Timed Systems Using Time-Abstracting Bisimulations. Form. Methods. Syst. Des., 18, pp. 25-68, 2001.
- We have added a loop with action
`busy`

on state`retry`

that is missing in the publication above. Without this loop, the system cannot exit the collision mode. Our model has 9 stations. Bigger or smaller instances are obtained by modifying the value of constant N. All other constants (L for lambda and S for sigma) have been set accordingly to the publication above. - FDDI protocol [fddi10.xml]
- Source: C. Daws, A. Olivero, S. Tripakis and S. Yovine. The tool KRONOS. Hybrid Systems III, Lecture Notes in Computer Science 1066, pp. 208-219, 1996.
- Since TChecker only supports resets of clocks to zero, we have
replaces every reset like
`x:=y`

by`x:=0`

. This involved duplicating states and transitions. Our model has 10 processes. Bigger or smaller instances are obtained by modifying the value of constant N. All other constants (TTRT, SA, TD) have been set accordingly to the publication above. - Fischer's mutual exclusion protocol [fischer7.xml]
- Source: S. Tripakis and S. Yovine. Analysis of Timed Systems Using Time-Abstracting Bisimulations. Form. Methods. Syst. Des., 18, pp. 25-68, 2001.
- Our model has 7 processes. Bigger or smaller instances are obtained by modifying the value of constant N. We have set constants k (Delta in the publication) and K (Lambda in the publication) to 10 which seems standard in timed automata benchmarks.
- Flexray physical layer
- Source: M. Gerke, R. Ehlers, B. Finkbeiner and H.-J. Peter. Model Checking the FlexRay Physical Layer Protocol. Formal Methods for Industrial Critical Systems - 15th International Workshop (FMICS), Lecture Notes in Computer Science 6371, pp. 132-147, 2010.
- Our model is written in C++ using TChecker libraries
- Lynch-Shavit mutual exclusion protocol [lynch10.xml]
- Source: MCMT benchmarks
- Our model has 10 processes. Bigger or smaller instances are obtained by modifying the value of constant N.

## Publications

PDF files can be downloaded from authors' webpages.

- F. Herbreteau and T.T. Tran. Improving search order for reachability testing in timed automata. Proc. 13th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS), 2015.
- F. Herbreteau and B. Srivathsan. Coarse Abstrations Make Zeno Behaviors Difficult to Detect. Logical Methods in Computer Science 9(1), 2013.
- F. Herbreteau, B. Srivathsan and I. Walukiewicz. Lazy abstractions for timed automata Proc. 25th Int. Conf. on Computer Aided Verification (CAV), 2013.
- F. Herbreteau, B. Srivathsan and I. Walukiewicz Efficient Emptiness Check for Timed Büchi Automata. Formal Methods in System Design, 40(2), pp. 122-146, Springer, 2012.
- F. Herbreteau, B. Srivathsan and I. Walukiewicz. Better abstractions for timed automata. Proc. 27th ACM/IEEE Symp. on Logic in Computer Science (LICS), 2012.
- F. Herbreteau, D. Kini, B. Srivathsan, I. Walukiewicz. Using non convex approximations for efficient analysis of timed automata. Proc. 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Leibniz International Proceedings in Informatics (LIPIcs), 2011.
- F. Herbreteau, B. Srivathsan. Coarse abstractions make Zeno behaviors difficult to detect. Proc. 22nd Int. Conf. on Concurrency Theory (CONCUR), 2011.
- F. Herbreteau, B. Srivathsan. Efficient On-The-Fly Emptiness Check for Timed Büchi Automata. Proc. of the 8th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), 2010.
- F. Herbreteau, B. Srivathsan and I. Walukiewicz. Efficient Emptiness Check for Timed Büchi Automata. Proc. of the 22nd Int. Conf. on Computer Aided Verification (CAV), 2010.