PAT: Process Analysis Toolkit

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

Monthly archives for May, 2009

02, Jun, 2009: PAT 2.5.0 is released!

What’s new in PAT 2.5.0

In this release, Real-Time System module is implemented in PAT, which supports the modeling and verification of real time systems. For the user interface, PAT added the support for I18N and new model wizard. Other updates include language enrichment, new GUI functions, new examples and bug fixing. The details are explained as follows.

Real-Time System Module
In this module, we study real-time systems which are specified compositional timed processes. Timed processes running in parallel may communicate through either a shared memory or channel communications. Instead of explicitly manipulating clock variables, a number of timed behavioral patterns are used to capture quantitative timing requirements, e.g., delay, timeout, deadline, waituntil, timed interrupt, etc. For such systems, a model checking algorithm can be used to explore on-the-fly all system behaviors by dynamically creating (only if necessary) and pruning clock variables (as early as possible), and maintaining/solving a constraint on the active clocks.

Compared to the standard CSP process primitives, Real-Time System module in PAT adds five time specific primitives, the wait, timeout, timed interrupt, deadline and waituntil as explained as follows.
Note: the time values in the 5 primitives can be arbitrary expressions with global constants/variables and process parameter. But the actual values of these expression must be intergers.

1 Wait Process
A wait process Wait[t] allows no communications for period t then terminates. The process Wait[t];P is used to represent P is delayed by time t.

2 Timeout Process
The timeout process P timeout[t] Q passes control to an exception handler Q if no event has occurred in the primary process P by some deadline t.
In details, the process (a -> P) timeout[t] Q will try to perform a -> P, but will pass control to Q if the a event has not occurred by time t, as measured from the invocation of the process.

3 Timed Interrupt Process
Process P interrupt[t] Q behaves as P until t time units elapse and then switches to Q.

4 Deadline Process
Process P deadline[t] is constrained to terminate within t time units.

5 Waituntil Process
The waituntil operator is a dual to deadline. Process P waituntil [t] behaves as P but will not terminate before t time units elapse. If P terminates early, it idles until t time units elapse.

Language Enrichment of CSP module
1 Guarded input channel:
c?[x+y+9>10]x.y-> P channel input with guard expression
For channel input c?[x+y+9>10]x.y, the top element on the buffer is retrieved and then assigned to local free variable x and y if the buffer is not empty, and the guard condition x+y+9>10 is true. Otherwise, it waits. Note that in channel input, you can write expressions after c?, but the expressions can not contain any global variables.

2 Interrupt process syntax is changed from P |> Q to P interrupt Q to make it easier to understand.

3 General Choice is added into Both CSP and RTS module. General choice is resolved by any event. External Choice is resolved by only visible events.

4 Conditional Choice if now will produce a tau event for the condition testing only. We added ifa (atomic condition choice), which will do the condition testing and first event of then or else branch atomically.

User Interface
1 I18N Support. PAT provides different user interface languages: Chinese (Simplied), Chinese (Traditional), English, Japanese, German and Vietnamense. You can switch between the languages under toolbar View->Languages. System will remember your choice in the next start. Other languages will be added if there is a request.

2 New Model Wizard. To help the users to quickly start composing models, PAT provides a New Model Wizard as listed as follows. Users can quickly generate model templates based on the selection of modeling language and templates.
You can launch the wizard in the dropdown list of new button.

3 In Simulator, user can adjust the tooltip popup delay in the toolbar: 5s, 10s, 20s, 40s, 60s.

4 LaTex generation is improved. PAT style file pat.sty is avaiable now.

5 Model submission function is added. Users can contribute to PAT project by clicking the “Submit Model to Author” button (after Save As Button) to submit their models.

PAT Console Update
1 PAT Concole adds the options for search depth. (requested by FALCIONI DAMIANO)
2 Console interface is added for all Modules. Users can specify the target module by using -csp, -rtm, -ws.

C# Library Update
1 In C# Library, methods can throw PAT runtime exception for invalid operations.
2 PAT Lib now should be included in the model using import key word rather than automatically including all libraries automatically to improve the performance.

Others
1 User manual is updated to latest implementation
2 Security protocol example is added.
3 Three Timed CSP examples are added: Railway crossing and Fischer’s Protocol for Mutual Exclusion, and Timed Bridge Crossing Example