PAT: Process Analysis Toolkit

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

Monthly archives for March, 2011

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();

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.

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

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


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