PAT: Process Analysis Toolkit

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

Posts in category Posts

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

15, Nov, 2011: PAT 3.4.1 (beta) is released!

15, Nov, 2011
1 BDD support for CSP module is ready for testing. Wild Variable is also supported.
2 RTS module supports guard and ifa now. Parsing will fail if timed process is immediately following the guard and ifa.
e.g., P = [cond](Wait[5]);
3 A number of bug fixing for parsers in all modules.
4 Skip checking inside sequential composition is added and improved for all modules.
5 using direct array in process arguments and call arguments are supported.
e.g.
var <IntArrayList> intList;
intList.Add([1, 2, 3, 4, 5]);
6 font fixing for 64bit Windows machine.

22, Sep, 2011: 2 Postdoc Research Fellow Positions Available on Model Checking and Security

Highly motivated applicants are being sought to work on developing model checking techniques. The postdocs will work with the software engineering and formal methods group at National University of Singapore on further developing the PAT toolkit (http://www.patroot.com).

PAT is a powerful self-contained framework for modeling, simulating, and verification. It has an extensible architecture so that new modeling language, abstraction techniques, and model checking techniques can be easily supported. Currently, 11 modules supporting different domains have been developed, covering concurrent, real-time, probabilistic, hierarchical systems. It offers a library of model checking algorithms for a variety of properties, e.g., reachability analysis, temporal logic verification, refinement checking, verification with fairness, zone abstraction, probabilistic model checking, etc. PAT has been applied to many case studies and successfully found previously unknown bugs. It has been adopted for research and teaching in multiple universities. More details about PAT can be found at http://www.patroot.com.

The applicant shall conduct research related to model checking techniques and security verification. Following list is the possible topics.

  1. Verify security systems: security protocols, web security, TPM, security device, etc.
  2. Software and assembly code verification.
  3. Code synthesis for security procotols.
  4. PAT optimization using techniques like distributed/parallel model checking, automated abstraction techniques (possibly domain specific), generalized symmetry reduction, etc.

The applicant will study the PAT framework, identify the suitable state reduction techniques, design/implement the techniques in PAT.

The position involves conducting basic research, developing tools, working as part of a research team, traveling, and giving presentations. The working language is English.

Candidate profile:
– A PhD in Computer Science or related areas is required.
– Expertise in Formal Methods, Model Checking technology and Security.
– Strong background in logic and discrete math.
– Strong programming skills (the language we are working with is C#).
– An established research record.

The post-doc positions are funded by large research projects in School of Computing and Temasek Laboratories, National University of Singapore.
The term is currently 3 years starting immediately and can be extended.
The salary range is around 60K-92K SGD pa (1 SGD = ~ 0.83 USD). Housing allowance may also be provided.

Interested applicants should send their CV to Dr. DONG, Jin-Song at dongjs@comp.nus.edu.sg and Dr. LIU, Yang at liuyang@comp.nus.edu.sg.