PAT: Process Analysis Toolkit

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

Posts in category Posts

PAT Tutorial is presented at Australian Safety Critical System Conference in Sydney

Pervasive Model Checking

PAT Tutorial is presented at ASE 2016

Build Your Own Model Checker with PAT

PAT group’s PhD students graduated

6 PhD students in PAT group have successfully graduated at NUS in 2015.

Congratulations to Dr. Bai Guangdong, Dr. Gui Lin, Dr. Liu Shuan, Dr. Liu Yan, Dr. Nguyen Truong Khanh (missed from the celebration lunch photo) and Dr. Shi Ling.

We also like to thank them and previous 2014/2013 PhD graduates Dr. Tan Tian Huat, Dr. Song Songzheng, Dr. Zhang Shaojie, Dr. Zhang Xian and Dr. Zheng Manchun for their great contributions to the PAT related research.

pat2015phds

14, May, 2015: Minor updates for PAT 3.5.1

We have issued some minor fixes and upgrades for PAT version 3.5.1.
This can be downloaded from the Download Page.

13, Aug, 2013: PAT 3.5.1 is released!

In this release, we publish the Timed Automata Module in PAT.
The details about this module can be found in the link.

28, Dec, 2012: PAT 3.5.0 is released!

Happy New Year! After half year’s development. PAT 3.5.0 is out.
After PAT 3.5.0, .NET framework 4.0 is required to run PAT.
There are a number of new features and bugs fixing in this version as list below.

Update of PAT 3.5.0

1 First, PAT is now running on .NET framework 4.0 in order to benefit from the newer library, particularly the parallel library in .NET 4.0.
We have done another round of code restructuring based on the new .NET framework.

2 GUI improvement
a) Simulator is supported to display all enabled events in all states or only enabled at the current active state.
b) Parsing without output parsed specification in the output window. When some model is very big, to output the string takes very long time.
This option could help to solve this problem.

3 BDD library performance improvement

4 Bug Fixing and improvement
Bug fixing for the exception due to non-boolean expression used in LTL property
Bug fixing for searching and parsing
Bug fixing for nested IndexedProcess
String Type Event in alphabet and hiding process
Comments highlighting in the assertions section of the model

New features coming up

1 Several Multi-core model checking algorithms (Nested DFS based, Tarjon SCC search based, with fairness condition) are implemented.
These algorithms will be avaiable soon.

2 Learning based composition verification algorithms library CELL. We have implemented a number of compositional verification algorithms
and learning algorithms. This library (with source code) will be released soon.

3 New modules coming: BPEL module, Timed Automata module, UML state machine module, security module. Stay tuned.

30, July, 2012: PAT 3.4.4 is released!

1 Bug fixing for all modules for deadlock checking and divergence checking for some special cases.
2 In simulator, a Simulate Trace button is added to allow users to write a script to perform automatic simulation. After clicking it, a textbox is shown where you can writre the event trace like phil.0.0, phil.0.1, eat.0 or a, b(5), tick. Each event is seprated by comma and b(5) means you can perform b 5 times.
3 In Editior, PAT also provides another way to open the imported library directly. You can select the imported library path and then right click the button, choose “open import/include file” function to open it. This funcation can recognize absolute path, relative path to the current model file and inside lib folder of pat installation.
4 In CSP module, C++ Code generation function is improved with hardware API support and socket channel support mapping from channels.
5 For simplicity, BDD is only supporting LTS and TA module now
6 TA module performance improvement
7 our PAT.BDD library has been publish at http://www.comp.nus.edu.sg/~pat/bddlib/
8 Stop button has better responsive for LTL (with fairness) verification during the counterexample searching.

15, April, 2012: PAT 3.4.3 is released!

1 A set of new refinement algorithms are implemented for CSP module and PCSP module (based on anti-chain technique). For CSP module, the performance improvement is substantial for some cases.
Hence we make the new verification algorithm as default engine for refinement checking.
2 Bug fixing for RTS module (Thanks Oguzcan Oguz for reporting a number of critical errors in RTS module)

3 Bug fixing and performance improvement for BDD support for CSP and RTS modules.
4 Bug fixing in CSP module code generation function.

4, Feb, 2012: PAT 3.4.2 is released!

1 Code generation is improved and supports of more syntax for CSP module (still beta version, based on QP platform)
2 BDD support for CSP module is improved. BDD doesn’t support encoding interrupt as an LTS but can encode it with compositional function.
3 Most BEEM database examples are added (work in progress)
4 RTS module bugs are fixed.
5 Monotonic engine for reachability with max or min value is added back
“Search Engine: Shortest Witness Trace using Breadth First Search with Monotonically With Value”
6 Reward calculation is supported in PRTS, and parser are improved in PRTS.
7 Indexed events are supported in all modules.
8 Macro definitions usage is improved for all modules.

Macro can take in parameters as defined below. When calling the macro, the keyword call is used. The macro expression can be any possible expression in PAT (if, local variable declarition, while, assignment).

#define multi(i,j) i*j;
System = if (call(multi, 3,4) >12 ) { a -> Skip } else { b -> Skip };

Note that following usage of macro definitions are also allowed in PAT, which means that macro definitions can be a fragment of code to be used in the model.

var x = 0;
var y = 0;
var z = 0;
#define reset1 {x = 0; y = 0};
#define reset(i) {x = i; y = i};
P = e1{z = 0; reset1} -> Skip;
Q = e2{z = 2; call(reset, 1)} -> Skip;

9 Atomic process semantics is updated
Since PAT 3.4.2, the semantics of atomic process changes a little bit. In the example below, before PAT 3.4.2, event a and d are enabled at the same time when process Sys starts. In PAT 3.4.2, only d is enabled because enabled atomic process has higher priority than enabled events. We did this change is to make the semantics for atomic process in real-time modules in PAT easy to express.

P = a -> atomic { b -> c -> Skip};
Q = atomic { d -> e -> f -> Skip};
Sys = P ||| Q

With this new syntax, parallel events can have priorities like a and d above.

In RTS module, atomic process can contain timing constructs now. Consider the following:
P = atomic{Wait[5]; a -> Skip} ||| Q;
Q = b -> Q;

The tau (time tick) transition geneated by by Wait[5] will have higher priority than b and the tau, and event a will be bundled together.

5, Jan, 2012: PAT 3.4.1 is released!

1 Code generation is supported for CSP module (beta version, based on QP platform)
2 BDD support for CSP module is done
3 Bitwise operator for integers is supported in all basic 5 modules: & (and), | (or) and xor (^)
4 Some BEEM database examples are added (work in progress)
5 RTS module parser update to support channel array and process parameter range
6 Parser bug fixing and macro is supported in all basic 5 modules
7 RTS non-zeno checking with zone abstraction performance improvement