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.

Others
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.