What’s new in PAT 2.2.0
In this release, PAT has added new language features, optimizations for grouped process, new model checking techniques for parametrized systems and so on (mainly for CSP module). The performance of both CSP and Web Service modules is doubled. New examples are added. The details are explained as follows.
Language Changes of CSP module
1) Variable range specification is supported.
Users can provide the range of the variables/arrays explicitly by giving lower bound or upper bound or both. In this way, the model checkers and simulator can report the out-of-range violation of the variable values to help users to monitor the variable values. The syntax of specifying range values are demonstrated as follows.
var knight : {0..} = 0;
var board : {0..10} = [3, 5, 6, 0, 2, 7, 8, 4, 1];
var leader[N] : {..N-1}; where N is a constant defined.
2) Synchronous Channel is supported: the channel output and its matching channel input are engaged together. The synchronous channel event will be displayed as c.exp for channel output c!exp and channel input c?x. To do synchronous channel communication, simply set the size of the channel to be 0. All the channel communications for non-zero channel are asynchronous.
3) Grouped interleaving and infinite interleaving is supported.
||| {50} @ P(); 50 P() running interleavingly.
||| {..} @ Q(); infinite number of Q() running interleavingly.
[] x:{0..2} @ ( (||| {x} @ P) ||| (||| {x} @ Q()); this is equivalent to (Skip|||Skip)[]((||| {1} @P()) ||| (||| {1} @Q()) ) [] ((||| {2} @P()) |||(||| {2} @Q()));
Note: ||| {0} @ P() is same as Skip.
4) Nested compositions are allowed.
[] x:{0..2} @ ( ||| y:{0..x} @ P(x, y))
5) Selecting operator is removed from the syntax for the performance reason. The selecting operator can be expressed by hiding operator easily. Hence, the expressiveness of the language is not reduced.
6) Error message is added in parsing for the trivial infinite systems, e.g., P() = a -> Skip || P();
Assertions Changes of CSP module
1) PAT now supports the following set of fairness. The options are enabled automatically if they are applicable. For the meaning of the fairness options please refer to the PAT manual.
- Annotated Fairness on individual events: wf, sf, wl, sl.
- Event-level weak fairness on whole system events
- Event-level strong fairness on whole system events
- Process-level weak fairness on whole system processes
- Process-level strong fairness on whole system processes
- Strong global fairness
2) Channels (including synchronous and asynchronous channel) can be queried in the LTL propositions.
[]<> “c!5”
[]<> “c?1”
[]<> “c.1” for synchronous channel communication
3) Model checking systems with infinite number of identical processes is supported in PAT. Furthermore, you can add the different fairness constraints
on the infinite systems in the verification. See the build-in examples of parametrized systems and PAT manual for more details..
Performance Improvement for All Modules
1) Evaluation for parallel and interleave are completely re-written
2) Strong global fairness implementation is improved.
3) Use more static variables to improve the performance
After some testing, we found that the verification speed is doubled for some cases.
User Interface
1) Verification window is simplified.
2) About dialog box shows the information about each module independently.
3) PAT Website is upgraded to the latest version of the TiddlyWiki.
New Examples
1) Four new examples are added to demonstrate the parametrized systems modeling and verification.
2) Travel Agent example is added for the Web Service Module.
Visit Today : 1
This Month : 5
This Year : 127
Total Visit : 51376
Hits Today : 529