CTAV: A Model Checking Tool  for Linear Temporal Properties of Timed Automata

　

CATV is a model checker for linear-time based temporal logic properties of timed automata. CTAV uses the UPPAAL system description language to describe system models and uses Time-Constraint LTL formulas to describe requirement specifications. Time-Constraint LTL is an extension of propositional linear temporal logic (PLTL) with atomic clock constraints added as atomic formulas. That is, a time-constraint LTL formula is an LTL formula with propositions or atomic clock constraints as its atomic formulas. For example, []<>(“P1.loc”/\“k>=2”/\“P1.x>4”) is a formula in CTAV if k is a global integer variable, P1 is a process, loc is a location of P1 and x is a local clock variable of P1.

For a given timed automaton M, and a given time-constraint LTL formula φ, CATV can check whether there exists an infinite run of M that satisfies the time-constraint LTL formula φ. If M has no such a run satisfying φ, then ¬φ is true in M.

Notice: This is an ongoing work and CTAV is still under the development. If you have any comments or feedback, please write to ligy (at) ios.ac.cn.

---

Download

　

· CTAV(CTAV.tar.gz) for Linux platform

　

---

Usage

　

1. tar zxvf CTAV.tar.gz

2. cd CTAV

3. running the shell script ‘startup’.

---

Last modified: 2010/04/25. Contact: ligy at ios.ac.cn