PAT: Process Analysis Toolkit

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

28, Aug, 2011: PAT 3.4 (beta) is released!

After 4 months, PAT 3.4.0 is ready now. We put this release as beta version as there are some system architecture changes which affects every module. The main update of this version includes the following.

Language Update:

  1. Accessing public properties/fields of C# objects using syntax like obj$property (can be read or write)
  2. PAT now supports channel arrays, which is a syntax suger to make the modeling easier if the channels are parameterized. The following syntax demonstrates how to use the channel array.

channel c[3] 1;
Sender(i) = c[i]!i -> Sender(i);
Receiver() = c[0]?x -> a.x -> Receiver() [] c[1]?x -> a.x -> Receiver() [] c[2]?x -> a.x -> Receiver();
System() = (||| i:{0..2}@Sender(0) ) ||| Receiver();
Note: Two or N dimentional channel array can be simulated by using 1 dimentional channel array. Hence, we don’t provide syntax support for that. For example channel c[3][5] 1 is same as channel c[15] 1, and c[2][3]!4 -> Skip is same as c[2*N+3]!4 -> Skip, where N is the first dimention.
3. Channel operations
PAT provides 5 channel operations to query the buffer information of asynchronous channels: cfull, cempty, ccount, csize, cpeek. The usage of these operations follows the normal static method call, i.e., call(channel_operation, channel_name).
cfull: test whether an asynchronous channel is full or not. e.g. call(cfull, c).
cempty: test whether an asynchronous channel is empty or not. e.g. call(cempty, c).
ccount: return the number of elements in the buffer of an asynchronous channel. e.g. call(ccount, c).
csize: return the buffer size of an asynchronous channel. e.g. call(cfull, c).
cpeek: return the first element of an asynchronous channel. e.g. call(cpeek, c).

GUI Update

  1. Verification window is redesigned. We remove all the options and check boxes with two selection: Admissible Behavior and Verification Engine. Admissible behavior offers the constraints on the model’s behavior; Verification engine offers the possible verification algorithms (with the reduction techniques).
  2. A new module generator is implemented. A simple editor is avaiable for developers to testing the code. You can acutally use this generated editor project for your module development. The code is minimum and compilation speed is very fast.
  3. UML console supported requested by the users.

Algorithm Update:

  1. BDD supports deadlock, reachability, LTL with fairness verfication now. See LTS module for the details.
  2. RTS module provides a new abstraction: digitalization. Users can select either zone abstraction or digitalization as the abstraction technique in verfication and simulation. For simulation, you can change the choice in the option window.
  3. CSP Module supports symbolic model checking using BDD

Performance Update:

  1. Performance improvement for RTS and PRTS modules

  1. BDD performance improvement for LTS module.

  1. NesC Module Improvement and new examples are added.

and a lot of bug fixings…