Real Time Studio (RT-Studio) is an integrated environment for the edition, simulation and automatic verification of real time systems modeled as networks of Interpreted Time Petri Nets (ITPNs). In its current version the tool proposes the construction of several abstractions for ITPNs suitable to verify their reachability, linear and branching properties. RT-Studio also integrates a classical CTL model-checker, an innovative TCTL model-checker based on a forward on the fly verification technique, and a minimizer under bisimulation. The environment is also intended as a general purpose simulation an verification tool for other extensions of Petri nets as it already allows to construct and simulate Interpreted Hybrid Functional Petri Nets (IHFPNs) for Biopathways analysis and continuous event system simulation. Other extension to the tool are also expected to support colored Petri nets and timed automata.

Last update: 07/05/2014

Download (windows version): RT-Studio-win-v1.17.zip

To install, unzip ‘RT-Studio-win-v#.zip’ in a directory of your choice.
To run, double click  RT-Studio.jar.

For any feedback please contact Dr. Rachid Hadjidj (rhadjidj@qu.edu.qa) or Dr. Hanifa Boucheneb (hanifa.boucheneb@polymtl.ca).

Video tutorials:

1. Installation instructions
2. Tool overview
   1. A simple TPN
   2. A simple Interpreted TPN
   3. Synchronizing Project components using places
   4. Synchronizing Project components using transitions
3. TCTL verification (comming very soon)
4. State spaces generation (comming very soon)
5. HFPN simulation (comming very soon)
6. A comparison with UPPAAL