PAT: Process Analysis Toolkit

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

Posts in category Posts

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.

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…

29, May, 2011: PAT Student Team won ICSE Score Formal Methods Award

PAT Student team (Li Yi, Yang Hang and Wu Huanan) won the Formal Methods Award in SCORE 2011 in Honolulu, Hawaii. There are only two awards: Formal Methods Award and Overall Award.

The system they developed is Transport4You, an intelligent public transportation manager, which employs formal methods during system design, implementation, testing and verification. PAT is used as a model checker and decision maker in the project.

Statistics for SCORE 2011: 94 registrations from 48 universities in 22 countries, 55 submissions, 18 selected for the second round, 5 finalist teams invited to ICSE.

27, April, 2011: PAT 3.3.1 is released!

In this release, we have the following updates:
1 The simulator drawing components are updated to the latest version of MSALG library.
2 Bug fixing and performance improvement for RTS and PRTS modules. RTS Module Experiments
3 BDD performance improvement for LTS module.
4 NesC Module Improvement and new examples are added.

18, March, 2011: PAT 3.3.0 is released!

This release mainly introduce more language syntax sugers, latest Antlr Parser library, GUI improvement and bug fixing.

Language changes:
1 The indexed booleans expressions are supported in CSP Module.
The indexed expression is a syntax sugar for grouping a list of OR or AND expressions together overal a range of variables. The syntax is following:
A typical example is as follows:
var x[3];
P = if(&& i:{0..2}@(x[i] == 0)){bingo -> Skip};

2 Index events are supported in CSP Module.
The syntax sugar indexed event list can be used in the definition of alphabets. For example:
#define N 2;
P = e.0.0 -> e.0.1 -> e.0.2 -> turns -> e.1.0 -> e.1.1 -> e.1.2 -> e.2.0 -> e.2.1 -> e.2.2 -> P;
#alphabet P { x:{0..N}; y:{0..N} @ e.x.y };

The above definitions define the alphabet of process P as the set of all events except event turns appearing in its proces definition.

The syntax sugar indexed event list can be used for defining a set of events with the same prefix. For example, the definition for process dashPhil() can be rewritten as the following.
dashPhil() = Phil() { x:{1..2} @ getfork.x, y:{1..2} @ putfork.y};

3 Warning is added for non-synchronization of events and data operations.
This is a common problem raised by many users that, for the following program, can the two processes P() and Q() synchronise on the event a? If not, then how to make them synchronise on ‘a’ and preserve the execution of statement block ({x++}) in an atomic fashion?
var x=0;
P() = a{x++} -> b -> P();
Q() = a -> c -> P();
System() = P() || Q();

Answer:
No-Synchronization on Data Operations is a design decision to void data race. If two data operations can synchronize, the update of the same global variable can lead to data race. Therefore, PAT will give a warning that if there one data operation and an event with same in different processes running in parallel.

Back to the question, a intuitive solution is to put the event ‘a’ and increment statement in an atomic action as follows:
P() = atomic{a -> update{x++} -> Skip};b -> Skip;
Q() = a -> c -> Skip;
aSystem() = P() || Q();

Then x will be updated right after a is engaged, and a will be synchronised.

The other possible solution could be:
P() = a -> update{x++} -> a1 -> b -> P();
Q() = a -> a1 -> c -> P();

4 Parsers are updated to the latest version of Antlr C# library.

GUI
1 Splash screen is added
2 Multi asseertion selection in the Model Checking
3 More high-lighting in the model checking output form
4 Bug fixing in the GUI

Examples
1 More examples are added in the LTS module.
2 Simulation Image is added to Kight Tour example in CSP Module

Bug Fixing
1 Bugs in external choices are fixed in all modules

13, March, 2011: Experiments for FSE 2011 are added!

Paper 68: PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers
Paper 84: Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare

Others

Experiments for FM 2011 Submissions

Paper 16: Developing a Model Checker for Probabilistic Real-time Hierarchical Systems
Paper 23: Compositional Partial Order Reduction for Concurrent Systems
Paper 40: Building Model Checkers Made Easy
Paper 58: Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare
Paper 61: Automated Verifying Anonymity and Privacy Properties of Security Protocols
Paper 101: On Combining State Space Reductions with Global Fairness Assumptions

28, Feb, 2011: PAT 3.2.3 is released!

In this minor release, the update include the following:
1 Parsers are all updated to the latest antlr library, as well as the error messages are improved.
2 In LTS module, BDD library execution error is fixed
3 Indexed Boolean logic expression is supported
e.g.
var x[3];
P = if(&& i:{0..2}@(x[i] == 0)){bingo -> Skip};

4 GUI improvement for the C# library Editor and Main GUI
5 PAT now will open the last edited documents when started
6 User Manual is updated.

21, Jan, 2011: PAT 3.2.2 is released!

In this minor release, the update include the following:
1 Bugs for simulator are fixed
2 Find Usage for variables, processes, channels and declarations are supported in all modules
3 Module Generator is implemented.
4 LTS module is re-implemented.
a) The language support full syntax of CSP, except terminal process call can only drawn Process. For example, the following syntax is not valid
P = a -> Skip;
Q = b -> P;
b) a new syntax is supported in LTS under the BDD module checking
var x = *; a process with arbitrary value

13, Jan, 2011: Experiments for FM 2011 are added!

Experiments for FM 2011 Submissions

Paper 16: Developing a Model Checker for Probabilistic Real-time Hierarchical Systems
Paper 23: Compositional Partial Order Reduction for Concurrent Systems
Paper 40: Building Model Checkers Made Easy
Paper 58: Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare
Paper 61: Automated Verifying Anonymity and Privacy Properties of Security Protocols
Paper 101: On Combining State Space Reductions with Global Fairness Assumptions