Posts in category Posts

4, Nov, 2009: PAT is presented FM 09

November 13, 2009 Written by admin

PAT team presented the following two papers in Formal Methods 2009 in Eindhoven, the Netherlands.

Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu and Jin Song Dong. Fair Model Checking with Process Counter Abstraction. The sixth International Symposium on Formal Methods (FM 2009). pages 123 – 139, Eindhoven, the Netherlands, November, 2009. (Slides)
Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. Model Checking Lineariability via Refinement. The sixth International Symposium on Formal Methods (FM 2009). pages 321-337, Eindhoven, the Netherlands, November, 2009. (Slides)

24, Oct, 2009: Warning List is supported. PAT makes the modeling easier!

October 24, 2009 Written by admin

How do I know that my model is correct?
Answer: After finishing your model, you can check the syntax of your model by clicking Check Grammar button. If your model is syntactically correct, PAT will display the parsed model in the output window in the bottom. You can check the parsed model to confirm that your model is the one you want. Note: sometimes, a missing bracket or simple typo can produce a different model.

All module parsers in PAT support error recovery, e.g., they can automatically add missing brackets or remove extra brackets or semi-colons. However, all error recovery information will be displayed as warnings in Error List window. You need to be careful if there are warnings after parsing, because the error recovery feature may parse the model to a different one than you want. We suggest you to clear out all warnings before doing any analysis.

30, Sep, 2009: PAT Japanese user group formed

October 9, 2009 Written by admin

Thanks to Prof. Kenji Taguchi from National Institute of Informatics, Japan. PAT had its first user group (in Japan) now. Anyone interested in joining or forming a user group, please do not hesitate to About Us.

25, Sep, 2009: PAT supports user defined data structures

September 25, 2009 Written by admin

PAT only
supports integer, Boolean and
integer arrays for the purpose of efficient verification.
However, advanced data structures (e.g., stack, queue, hashtable and so
on) are necessary for some models. To support arbitary data structures, PAT
provides an interface to create user defined data type by inheriting an
abstract classes
ExpressionValue.

The
following is one simple example showing how to create a hashtable
in C#.

using System.Collections;
using
PAT.Common.Classes.Expressions.ExpressionClass;

//the namespace must be PAT.Lib, the class and method names can
be arbitrary
namespace PAT.Lib {
public class
HashTable : ExpressionValue
{
public Hashtable
table;

        /// Default
constructor without any parameter must be
implemented
        public HashTable()
{

table = new Hashtable();

}

        public
HashTable(Hashtable newTable)
{

table = newTable;

}

        public void Add(int
key, int value)
{

if(!table.ContainsKey(key))
{

table.Add(key,
value);

}

}


        public bool ContainsKey(int
key)
{

return
table.ContainsKey(key);

}

        public int
GetValue(int key)
{

return (int)table[key];

}

        /// Return the
string representation of the hash
table.
        /// This method must
be overriden
        public override
string ToString()
{

string returnString =
“”;

foreach (DictionaryEntry entry in table)
{

returnString += entry.Key + “=” + entry.Value +
“,”;

}

return returnString;

}

        /// Return a deep
clone of the hash table
        ///
This method must be
overriden
        public override
ExpressionValue GetClone()
{

return new HashTable(new
Hashtable(table));

}

        /// Return the
compact string representation of the hash
table.
        /// This method must
be overriden
        /// Smart
implementation of this method can reduce the state space and speedup
verification
        public
override string GetID()
{

string returnString =
“”;

foreach (DictionaryEntry entry in table)
{

returnString += entry.Key + “=” + entry.Value +
“,”;

}

return returnString;

}

}
}

Note the
following requirements when you create your own data structure
objects:

The
namespace must be “PAT.Lib”, otherwise it will not be recognized. There is no
restriction for class names and method
names.
Importing the PAT Expression name
space using “using
PAT.Common.Classes.Expressions.ExpressionClass;“.
Only
public methods can be used in PAT models
The
parameters must be of type “bool”, “int”, “int[]” (int array) or object
(object type allow user to pass user defined data type as
parameter).
The
number of parameters can be 0 or many.
The
return type must be of type “void”, “bool”, “int”, “int[]” (int
array) or user defined data type.
The
method names are case sensitive.
Put
the compiled dlls in “Lib” folder of the PAT installation directory to make
the linking easy by using #import
“DLL_Name”;

if your
methods need to handle exceptional cases, you can throw PAT runtime
exceptions as illustrated as the following example.

public static int StackPeek(int[] array)
{
if (array.Length >
0)
return
array[array.Length – 1];

//throw PAT Runtime
exception
throw new
PAT.Common.Classes.Expressions.ExpressionClass.RuntimeException(“Access an
empty
stack!”);
}

To
import the libraries in your model, users can using following
syntax:

#import “PAT.Lib.Hashtable”; //to import a library under
Lib folder of PAT installation path
#import
“C:Program FilesIntelHashtable.dll”; //to import a library using absolute
path

To
declar the user defined types in your models, please use the following

syntax:

var<HashTable> table; //use the class name here
as the type of the varaible.

To
invoke the public methods in your models, please use the
following syntax:

table.Add(10, 2);
if(table.ContainsKey(10))…

05, Sep, 2009: PAT 2.7.0 is released!

September 5, 2009 Written by admin

What’s new in PAT 2.7.0

In this release, the main achievement is that timed refinement checking algorithm is implemented in Real-Time System (RTS) module. At this stage, all the planned algorithms are implemented in RTS module. In the future, we will work on the syntax enrichment and performance improvement for RTS module. In this release, modeling languages in CSP and RTS modules are improved for better expressiveness power and parsing precision. Other updates include new examples and bug fixing.

Timed Refinement
Sometimes timing aspects are important in the system requirment, e.g., human heart must beat at rate between 50/minute to 200/minute (too low or too high is vital for human lifes). In these cases, we can use time refinement to check whether the input model follows the desired timing requirement. The syntax is the following:

#assert Implementation() refines< T> TimedSpec() ;

Note: For timed refinement checking, RTS module uses a timed trace semantics (i.e. a mapping from a model to a set of finite timed event sequences) and a timed trace refinement relationship (i.e. a model satisfies a specification if and only if the timed traces of the models are a subset of those of the specification). The verification algorithm developed for timed refinement checking will verify that a system model is consistent with a specification by showing a refinement relationship. A timed event sequence is presented as a counterexample if there is no such refinement relationship. For the timed refinement checking, PAT requires that the implementation or specifications are not divergent, otherwise the shared clock will not be bounded. If the system is divergent, PAT will ask user to provide a ceiling for the shared clock (default is 2^15).

Process Parameters are Supported in Grouped Processes
In order to have better compositional behaviors, we allow process parameters to be used in in grouped processes. For example, in []x:{0..n}@P or ||| {0} @ P() , n can be a global constant or process parameter, but not a global variable. We make this restriction for the performance reason. For example, the following definitions are all valid in PAT.
#define n 10; |||x:{0..n}@P;
P(n) = |||x:{0..n}@Q;

Channel Names can be Used as Event Names
Event name is an arbitrary string of form (‘a’..’z’|’A’..’Z’|’_’) (‘a’..’z’|’A’..’Z’|’0′..’9’|’_’)*. However, global variable names, global constant names, process names, process parameter names, propositions names can not be used as event name. One exception is the channel names are allowed, because we may want to use channel name in specification process to simulate the channel behaviors and use refinement checking to compare with real channel events.

Divergence-free
Given P() as a process, the following assertion asks whether P() is divergence-free or not.
#assert P() divergencefree;
Given a process, it may performs internal transitions forever without engaging any useful events, e.g., P = (a -> P) {a};, In this case, P is said to be divergent. Divergent system is ususally undesirable.

Timed Divergence-free
Given P() as a process, the following assertion asks whether P() is timed divergence-free or not.
#assert P() divergencefree< T>;
Given a process, it may performs internal transitions and timed transitions forever without engaging any useful events, e.g., Q = (a -> Wait[5]; Q) {a};, In this case, P is said to be timed divergent. Timed divergent system is undesirable, which can give unbounded timer, which disallows timed refinement checking.

Note: P = (a -> P) {a}; is divergent, but not timed divergent, because it performs internal transitions forever without timed transitions.

Others
1 User manual is updated to latest implementation.
2 Real-Time system examples (Timed PaceMaker) and timed refinement assertions are added.
3 Fix the bugs in parsing, GUI and other places.

150 countries and regions

June 12, 2009 Written by admin

Afghanistan
Albania
Algeria
Andorra
Angola
Antigua & Deps
Argentina
Armenia
Australia
Austria
Bahamas
Bahrain
Bangladesh
Barbados
Barbuda
Belarus
Belgium
Benin
Botswana
Brazil
Bulgaria
Burkina
Cambodia
Cameroon
Canada
Cape Verde
Chad
Chile
China
China, Macao
China, Taiwan
Colombia
Congo
Costa Rica
Croatia
Cuba
Czech Republic
Denmark
Ecuador
Egypt
El Salvador
Equatorial Guinea
Estonia
Fiji
Finland
France
Georgia
Germany
Ghana
Grenada
Guatemala
Haiti
Honduras
Hong Kong
Hungary
Iceland
India
Indonesia
Iran
Iraq
Ireland
Ireland (Republic)
Israel
Italy
Ivory Coast
Jamaica
Japan
Kazakhstan
Kenya
Khi
Korea South
Kosovo
Kuwait
Kyrgyzstan
Lebanon
Liberia
Luxembourg
Macedonia
Malawi
Malaysia
Mali
Malta
Marshall Islands
Mauritius
Mexico
Moldova
Monaco
Mongolia
Morocco
Mozambique
Myanmar (Burma)
Namibia
Nepal
Netherland
New Zealand
Nicaragua
Niger
Nigeria
Northern Ireland
Norway
Oman
Pakistan
Pakistan?
Palau
Panama
Paraguay
Peru
Philippines
Poland
Portugal
Qatar
Reunion
Romania
Russia
Russian Federation
Saint Vincent & the Grenadines
Saudi Arabia
Senegal
Serbia
Sierra Leone
Singapore
Slovak Republic
Slovakia
Slovenia
Somalia
South Africa
South Korea
Spain
Sri Lanka
St Kitts & Nevis
Sweden
Switzerland
Syria
Thailand
Tonga
Trinidad & Tobago
Tunisia
Turkey
Turkmenistan
U.S.A.
Uganda
Ukraine
United Arab Emirates
United Kingdom
United States
Uruguay
Venezuela
Vietnam
Zambia
Zimbabwe

09, Jun, 2009: PAT 2.6.0 is released!

June 9, 2009 Written by admin

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

02, Jun, 2009: PAT 2.5.0 is released!

May 29, 2009 Written by admin

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

30, Apr, 2009: http://www.patroot.com is online

April 30, 2009 Written by admin

We registered a new domain name for PAT: http://www.patroot.com. Later on, we will graduately move the website under this domain. Currently it will redirect to http://www.comp.nus.edu.sg/~pat/

30, Apr, 2009: PAT 2.4.0 is released!

April 30, 2009 Written by admin

What’s new in PAT 2.4.0

In this release, PAT has gone through a complete system re-design such that classes for Label Transition System, all model checking algorithms, common utility functions and simulator are centralized in PAT Common project, which can be shared by all modules. This design allows new modules to be created easily by simply creating parser, module specific language construct classes and model checking user interface.
Other updates include language enrichment, new GUI functions, new examples and bug fixing. The details are explained as follows.

Language Enrichment of CSP module
1 Quick array initialization: To ease the modeling, PAT supports fast array initialization using following syntax.

#define N 2;
var array = [1(2), 3..6, 7(N*2), 12..10];
the above is same as the following
var array = [1, 1, 3, 4, 5, 6, 7, 7, 7, 7, 12, 11, 10];

In the above syntax, 1(2) and 7(N*2) allow user to quickly create an array with same initial values. 3..6 and 12..10 allow user to write quick increasing and decreasing loop to initialize the array.

2 Process Counter Variable is Supported
User can define a special variable for a process to keep track of the number of the process in the system. This variable is very helpful when modeling of system with infinite number of identical processes so that we can use and check the number of identical processes. One example is following.

#define noOfReading #Reading();
var writing = false;

Writer() = [noOfReading == 0 && !writing]startwrite{writing = true;} -> stopwrite{writing = false;} -> Writer();
Reader() = [!writing]startread -> Reading();
Reading() = stopread -> Reader();

ReadersWriters() = |||{..} @ (Reader() ||| Writer());

3 PAT added the support for two assignment syntax sugars ++, —. x++ is same as x=x+1. y— is same as y = y-1. y=x++ is same as x = x +1; y = x;. There are no shorthands for other shorthands, such as ++b , — b , b *= 2 , b += a , etc. Where needed, their effect can be reproduced by using the non-shortened equivalents, The following example shows the usage of ++ and —, where the final values of x and y are both 3.

var x = 2; var y;
P() = add{x ++;} -> minus{x — ;} -> event{y=x++;} -> Skip;

4 Event local variables are supported. The scope of the local variable is only inside the sequential program and starts from the place of declaration.

var array = [0,2,4,7,1,3];
var max = -1;

P() = findmax{
var index = 0;
while (index < 6) {
if (max < array[index]) {
max = array[index];
}
index = index+1;
};
} -> P();

Language Enrichment of Wes Service module
1 We implemented all the language features of CSP module to WS module: local variable, multi-dimensional array, array initialization and so on.
2 Channel communication allow multiple data to be passed
3 Synchronous Channel communication is supported.

User Interface
1 Bugs for text drag and drop are fixed
2 Tab navigation functions are supported: Go to Previous Tab (Ctrl+Shift+Tab), Go to Next Tab (Ctrl+Tab)
3 Drag and Drop an external model into PAT to open it quickly.
4 Simulator is shared by all modules

User manual is updated to latest implementation
1 FAQ section is added in the manual. We will add more questions asked by the users.