PAT: Process Analysis Toolkit

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

Monthly archives for June, 2009

87 countries and regions

Afghanistan
Albania
Algeria
Andorra
Angola
Argentina
Australia
Austria
Bangladesh
Barbados
Barbuda
Belarus
Belgium
Botswana
Brazil
Bulgaria
Cameroon
Canada
Chile
China
China, Macao
China, Taiwan
Colombia
Czech Republic
Denmark
Egypt
El Salvador
Estonia
Fiji
Finland
France
Germany
Haiti
Hong Kong
Hungary
India
Indonesia
Iran
Ireland
Israel
Italy
Jamaica
Japan
Kazakhstan
Khi
Korea South
Luxembourg
Macau
Macedonia
Malaysia
Mexico
Moldova
Netherland
Netherlands
New Zealand
Nigeria
Norway
Pakistan
Pakistan‎
Palau
Philippines
Poland
Reunion
Romania
Russia
Saudi Arabia
Senegal
Singapore
Slovak Republic
Slovakia
South Africa
South Korea
Spain
Sweden
Switzerland
Syria
Thailand
Tunisia
Turkey
U.S.A.
Ukraine
United Arab Emirates
United Kingdom
United States
Uruguay
Vietnam
Zambia

09, Jun, 2009: PAT 2.6.0 is released!

What’s new in PAT 2.6.0

In this release, Real-Time System module is improved with more timed syntax. Atomic events sequence is supported in CSP and RTS module. For the user interface, PAT provides a better document management menu in the Window toolbar. The simulator’s graph generation is put into an additional thread, which will not hang the user interface. Other updates new examples and bug fixing.

Atomic Sequence

The keyword atomic allows user to define a process which always makes maximum progress if possible. The syntax is atomic{P}, where P is any process definition.

If a sequence of statements is enclosed in parentheses and prefixed with the keyword atomic, this indicates that the sequence is to be executed as one super-step, non-interleaved with other processes. In the interleaving of process executions, no other process can execute statements from the moment that the first statement of an atomic sequence is executed until the last enabled one has completed. The sequence can contain arbitrary process statements, and may be non-deterministic.

Before atomic sequence starts, it competes with other processes. Once atomic sequence starts, it goes into the active state, and it continues to execute until termination or blocked. If any statement within the atomic sequence is blocked (e.g., due to a synchronous channel output event or parallel barrier synchronization), atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence is resumed immediately. If multiple active atomic processes are enabled, then they execute interleavingly. In the following example, process P(or Q) will be blocked by the synchronization channel event once they are in the active states. After the synchronization event, both P and Q are in active states, then the b -> c -> Skip and e -> f -> Skip are executed as there is no atomic.

channel ch 0;
P = atomic { a -> ch!0 -> b -> c -> Skip};
Q = atomic { d -> ch?0 -> e -> f -> Skip};
Sys = P ||| Q;

Note: atomic sequences can be used for state reduction for model checking, especially if the process is composed with other processes in parallel. The number of states may be reduced exponentially. In a way, by using atomic, we may partial order reduction manually (without computational overhead).

Note: atomic sequences inside other atomic sequence has no effect at all.

Note: Atomic sequence is supported in RTS module, all the engaged events in atomic group takes no time.

Syncrhonous Channel in LTL
In LTL, if there is synchronous channel, its input (?) or output (!) event will be renamed to synchronous event (.) after parsing.
[](c1!2 -> <> c2?3) will be changed to [](c1.2 -> <> c2.3)

User Interface Update
1 Tab Management under Window toolbar, which provides similar behaviors like other IDE.
2 The graph generation function in Simulator is moved to an independent thread. The simulator will not hang when u generate a big graph.
3 Open file dialog box will use the default modeling language file type as the default file filter.

Others
1 User manual is updated to latest implementation.
2 Real-Time system example is added.
3 Fix the bugs in latex generation functions and change the “refines”, “refines<F>” and “refines<FD>” symbols in latex