Monthly archives for July, 2010

1, Aug, 2010: PAT 3.1.0 is released. PAT is cross-platform now: running on Linux, Mac OS and more!

July 30, 2010 Written by admin

After some efforts, we glad to release PAT 3.1.0, which can run in all platforms: Linux, Mac OS and more!
The solution is to use Mono, which is an open source, cross-platform, implementation of C# and the CLR that is binary compatible with Microsoft.NET.

Install PAT 3.x in Linux, Unix, Mac OS or more, please follow these steps:

You should install mono tool in your system which is freely available. Please download from here according to your OS.
Download PAT 3.x. But choose the directly executable version to some place in your computer.
In your computer, start terminal application, using the command cd to the directory where you put “PAT 3.exe”;
Type the command mono “PAT 3.exe” into terminal. Bingo! You will see the GUI of our PAT.

Note that running PAT in Mono, the performance can be (much) slower than runing PAT in Windows.
Here is some prelimenary experiment on the CSP linearizability Stack example, with same laptop but different OS.

Mac OS

Windows

stack length: 875.39s24.69sstack length: 986.42s30.74sstack length: 10111.04s39.55s

There are some known bugs when running PAT in Mono:
1) Email sending in Mac OS is not working. This is an issue of Mono library.
2) Sometimes the first line of the model (or part of the model) is invisible, and user should click there to see the text.
3) in simulation window, it works very well except the Save and Export buttons. These two buttons are invisible before you click them.

If you find bugs and issues when running PAT in Mono, please do About Us.

Other update in the version 3.1.0 including bug fixing and new examples.

Posts

14, July, 2010: PAT 3.0.0 is released!

July 14, 2010 Written by admin

After some testing, PAT 3.0 is arrived. Compared with the beta version, we mainly do the bug fixing.

New features in the RTS module:
Urgent Event

In RTS module, we assume all the event prefix, data operation and channel communication (channel input/channel output) takes arbitrary amount of time. Sometimes, we want the events takes no time (instantaneous events). The normal approach is to use (Process within[0]) to model this requirement. In RTS module, we introduce the concept of Urgent Event to simplify this kind of modeling. The supported syntax is shown in the following examples.

event{program} ->> Process

c!x ->> Process

c?x ->> Process

Note: tau event in RTS module is an urgent event by default. A natural consequence is that, all events after hiding become tau event and take no time.

Timed Zenoness Checking

Because RTS module supports process constructs like deadline, it suffers from zeno executions, i.e., infinitely many steps taking within finite time. Zeno executions are unrealistic and therefore must be ruled out in model checking. It is known that zone graphs are not fine enough to distinguish zeno executions. We show that the zone graph produced by dynamic zone abstraction can be modified so that the properties are verified with the assumption of non-Zenoness.

To remove zeno executions, PAT implements Zeno checking for LTL/Deadlock assertions. Users only need to tick the “Apply Zeno Check” in the model checking form. More Zeno checking will be implemented for RTS module.

Posts