PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

TA Module

TA module in PAT is designed to verify systems which can be modeled as
networks of timed automata extended with shared variables, structured data types, user defined functions, and channel synchronization.
The following demonstrates the experimental results on embedded examples
in TA module and UPPAAL as well as the explanations of experiment

We run experiments on four models, namely, Fischer protocol, railway
control systems, FDDI protocol and CSMACD protocol to verify properties
such as deadlock-freeness, liveness, reachability and so on. The
following table summarizes the verification results. Here, ‘Proc’ means
the number of interleaving processesand ‘-‘ means out of memory or more
than 2 hours. We also do the comparison work with UPPAAL, and here ‘UPPAAL-r’ means a recvised version of the original models in UPPAAL to make them consisten with the models in PAT, ‘State-s’ means the bumber of stored states,
‘State-e’ means the number of explored states. The environment of experiments ruuning on UPPALL 4.1.2 is as follows:

  1. Use convex-hull approximation
  2. Hash table size 16M
  3. Automatic extrapolation operator
  4. Depth First Search
  5. Conservative space consumption
  6. Enable sweepline method
  7. Enable peephole optimiser
  8. Enable symmetry reduction

  9. From the above table, we can see that PAT TA module can verify a rich set of priorities with reasonable time. In addition, some abservations are here:
    firstly, we can see that the number of states and
    running time increase rapidly with increasing the number of processes,
    e.g., 8 processes in Fischer model vs. 9 processes. Secondly, PAT is
    efficient and can handle million states in less than one hour. Thirdly,
    in some case, PAT is slower than UPPAAL. The main reason of UPPAAL outperforming
    PAT is that UPPAAL has benefied from many dedicated optimization techniques such
    as extrapolation, while PAT has none yet. The experiment data is available here.