PAT: Process Analysis Toolkit

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

Posts in category Posts

22, Sep, 2010: Two Posrdoc Positions on Model Checking at National University of Singapore

Two Postdoc Research Fellow Positions on Model Checking
National University of Singapore

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 (

PAT is a powerful self-contained system for modeling, simulating, and verification. It has an extensible architecture so that new modeling language, abstract techniques, and model checking techniques can be easily supported. Six modules supporting different domains have been develoed, covering concurrent, real-time, probabilistic, hierachical 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

The applicant shall conduct research on optimizing PAT. Candidate techniques include 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 lanugage is English.

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

The term is currently 2 years starting immediately and can be extended.
The salary range is around 60K-85K SGD pa (1 SGD = ~ 0.75 USD).

Interested applicants should send their CV to Dr. Jin-Song Dong at

2, Sep, 2010: PAT 3.2.0 (beta) is released!

PAT 3.2.0 is a beta version, which includes a lot of new modules: Labeled Transition Systems Module, Timed Automata Module, Orc Module, Security Module, NesC Module, MDL Module.

This version is a preview version and will not be avaiable from auto-update.
We will keep on updating this beta version to fix the bugs and complete the user manual.

Note that PAT 3.2.0 is restricted to academic use only.. If you want to use it for commertial purpose, please contact us.

1, Aug, 2010: PAT 3.1.0 is released. PAT is cross-platform now: running on Linux, Mac OS and more!

After some efforts, we glad to release PAT 3.1.0, which can run in all platforms: Linux, Mac OS and more!
The solution is to use Mono, which is an open source, cross-platform, implementation of C# and the CLR that is binary compatible with Microsoft.NET.

Install PAT 3.x in Linux, Unix, Mac OS or more, please follow these steps:

  • You should install mono tool in your system which is freely available. Please download from here according to your OS.
  • Download PAT 3.x. But choose the directly executable version to some place in your computer.
  • In your computer, start terminal application, using the command cd to the directory where you put “PAT 3.exe”;
  • Type the command mono “PAT 3.exe” into terminal. Bingo! You will see the GUI of our PAT.

Note that running PAT in Mono, the performance can be (much) slower than runing PAT in Windows.
Here is some prelimenary experiment on the CSP linearizability Stack example, with same laptop but different OS.

Mac OS Windows

stack length: 875.39s24.69sstack length: 986.42s30.74sstack length: 10111.04s39.55s


There are some known bugs when running PAT in Mono:
1) Email sending in Mac OS is not working. This is an issue of Mono library.
2) Sometimes the first line of the model (or part of the model) is invisible, and user should click there to see the text.
3) in simulation window, it works very well except the Save and Export buttons. These two buttons are invisible before you click them.

If you find bugs and issues when running PAT in Mono, please do About Us.

Other update in the version 3.1.0 including bug fixing and new examples.

14, July, 2010: PAT 3.0.0 is released!

After some testing, PAT 3.0 is arrived. Compared with the beta version, we mainly do the bug fixing.

New features in the RTS module:
Urgent Event

In RTS module, we assume all the event prefix, data operation and channel communication (channel input/channel output) takes arbitrary amount of time. Sometimes, we want the events takes no time (instantaneous events). The normal approach is to use (Process within[0]) to model this requirement. In RTS module, we introduce the concept of Urgent Event to simplify this kind of modeling. The supported syntax is shown in the following examples.

event{program} ->> Process

c!x ->> Process

c?x ->> Process

Note: tau event in RTS module is an urgent event by default. A natural consequence is that, all events after hiding become tau event and take no time.

Timed Zenoness Checking

Because RTS module supports process constructs like deadline, it suffers from zeno executions, i.e., infinitely many steps taking within finite time. Zeno executions are unrealistic and therefore must be ruled out in model checking. It is known that zone graphs are not fine enough to distinguish zeno executions. We show that the zone graph produced by dynamic zone abstraction can be modified so that the properties are verified with the assumption of non-Zenoness.

To remove zeno executions, PAT implements Zeno checking for LTL/Deadlock assertions. Users only need to tick the “Apply Zeno Check” in the model checking form. More Zeno checking will be implemented for RTS module.

30, May, 2010: PAT Forum is up!

Search and Post your questions in the forum:

22, May, 2010: PAT 3.0.0 beta is released!

What’s new in PAT 3.0.0

In this version, we have done a complete system redesign for better extensibility.

PAT’s UI is complete re-implemented with new text editor with improved syntax highlighting and input intellesense.

The performance of almost all assertions is improved compared with old version.

Beta version of PRTS Module is released. This module combines Probability and Real-Time for modeling Real-time probabilistic systems.

Important Note: PAT 3.0.0 is upgrated to .NET framework 3.5. To run PAT, you need to install .NET framework 3.5, which can be downloaded here.

18, March, 2010: PAT 2.9.1 is released!

What’s new in PAT 2.9.1

In this minor release, we introduced two new assertion: nonterminating and deterministic. Also a lot of bugs in CPS, RTS and PCSP modules are fixed. The most significant change is the Graph difference comparison function of any two simulation graph, which is a joined work with Dr Xing ZhenChang.


Given P() as a process, the following assertion asks whether P() is deterministic or not.

#assert P() deterministic;

Where both assert and deterministic are reserved keywords. Given a process, if it is deterministic, then for any state, there is no two out-going transitions leading to different states but with same events. E.g, the following process is not deterministic.

P = a -> Stop [] a -> Skip;


Given P() as a process, the following assertion asks whether P() is nonterminating or not.

#assert P() nonterminating;

Where both assert and nonterminating are reserved keywords. PAT’s model checker performs Depth-First-Search or Breath-First-Search algorithm to repeatedly explore unvisited states until a terminating state (i.e., a state with no further move, including successfully terminated state) is found or all states have been visited. The following process is deadlockfree, but not nonterminating.

P = a -> Skip;

Graph Difference Comparison
To compare the diffference between any two simulation graph can give user the feedback for the difference of the specifications.

In this version, we have implemented the first version of graph comparison of any two opened simulators. After the comparison, the differernce are highlighted in different colors.

16, March, 2010: Appreciation for PAT Japanese User Group

We would like to thank PAT Japanese User Group for supporting the PAT development (by providing Japanese translation and valuable feedback), promoting PAT tool and hosting us in Japan. We have special thank to Kenji Taguchi, Hiroshi Fujimoto, Masaru Nagaku, Toshiyuki Fujikura. We wish to extend the collaboration and achieve more fruitful results.

29, Jan, 2010: PAT 2.9.0 is released!

What’s new in PAT 2.9.0

In this release, there are three new modules are released: Probability CSP Module, Orc Module and NesC module. There are a lot of changes from the user interface, language syntax and verification algorithms. So we decide to make it a beta release before it becomes stable.

Probability CSP Module
PCSP module extends CSP module with probabilistic behaviors. With the introducting of probability choice in the modeling, PCSP module supports the verification of deadlock, reachability and LTL properties with probability queries.

Orc Module
Orc module supports the modeling and verification of Orc language, developed by the UT austin university. This is a beta release. More examples and testing are needed.

NesC module
NesC module supports the modeling and verification of NesC language. This is a beta release. More syntax of NesC language will supported soon.

Language Changes
1 with clause is supported in CSP module, RTS module and PCSP module for reachability properties.
To further query about variable values, PAT allows user to find the minimum value or maximum value of some expressions in all reachable traces. The following coin changing example show how to minimize the number of coins during the reachability search.

var x = 0;
var weight = 0;
P() = if(x <= 14)
coin1{x = x + 1; weight =weight + 1;} -> P() [] coin2{x = x + 2; weight = weight + 1;} -> P() [] coin5{x = x + 5; weight = weight + 1;} -> P()
#define goal x == 14;
#assert P() reaches goal with min(weight);

2 ‘new’ keyword is supported for the user defined data structures.
Var<HashTable> x = new HashTable(100);

3 ‘byte’ ‘short’ are supported in the return type of user defined methods.
But not supported for the method parameters.

3 nested if-then-else are supported
if (cond) { P } else if (cond2) { Q }

GUI updates
The search depth option is removed from the verifier. We implement the shortest witness trace option to find the shortest counterexample or witness trace for deadlock, reachability and refinement checks. The shortest witness searching algorithms are based on Breadth First Search.

The simulator is added with the option of hiding tau events.

Performance Improvement
1 Refinement verification algorithm is updated and improved.
2 Parallel execution is simplied.

1 User manual is updated to latest implementation.
2 Bug fixing in refinement checking algorithm
3 Bug fixing in LTL safety checking algorithm
4 LTL safety checking algorithms are implemented.
5 Examples are added for PCSP module and RTS module.
6 Parsers are improved for some error input.

02, Dec, 2009: PAT 2.8.0 is released!

What’s new in PAT 2.8.0

In this release, the main achievement is that safety properties detection and verification is implemented in PAT (in all modules). Furthermore, modeling languages in CSP and RTS modules are improved for better expressiveness power and parsing precision. Other updates include new examples and bug fixing.

Safety property detection
Safety properties verification is relatively easy and fast. However, sometimes it is hard to tell whether a LTL property is a safety one or liveness one. In this release of PAT, we implement the safety property detection algorithm to distinguish them from liveness ones. For all safety properties, we implemented a simple DFS model checking algorithm to speedup the verification. All these are automatic.

Assertion process is supported in all modules
Assertion process allows user to add an assertion in the program and PAT simulator and verifiers will check the assertion at run time. If the assersion is failed, a PAT runtime exception will be thrown to the user and the eveluation is stoped. The syntax of Assertion is as follows,

var x = 1;
P = assert(x > 0); e{x = x-1;} -> P;

Parsing warning is added for if/while expression inside event assignment with no body

LTL to Buchi Automata Converter is added into the UI
We provide a simple ultility under toolbar “Tools” to allow user to generate a BA from LTL directly.

1 User manual is updated to latest implementation.
2 Ctrl + W is supported to close the current tab.
3 UI exceptions are captured3 Fix the bugs in parsing, GUI and other places.