CTA-based Verifier for Reachability Analysis: CTAV/Reach 

     CTAV/Reach is a model checking tool for real time system, based on the integer semantics of closed timed automata. It supports the verification of real-time systems with multi-processes, synchronizations, and broadcasts.

    The tool set comprises the compiler for model and its property description, and the verifier. Currently executable files for Windows and Linux are available.
   
 

Downloads:

Windows: ReachModelChecker

Linux:  Executable File with static libraries;

        Dynamic compiling with makefile.

Examples including

  • Fischer's mutual exclusive protocol
  • CSMA/CD protocol
  • FDDI protocol

ReadMe outlines the instructions for execution.

If you find any bugs, please email to {ligy,yrj} at ios.ac.cn.

Last modified: 2007/04/26
กก