Welcome to TiddlyWiki created by Jeremy Ruston, Copyright © 2007 UnaMesa Association
!''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
After some effort, we come up some archetecture improvement:
1 Assersion checking is separated into independed class.
2 Data Manager is introduced, which supports of difference way of storing the states information.
Currently, we are testing for different way of hashing the states. Truong Khanh is working on the tree data structure at the moment.
In the GUI, user can select the different data manager for different purpose.
Syntax improvement:
1 Parser is upgraded to antlr 3.1
2 Language syntax is improved to support if-then-else (syntax suger for conditional choice), case swith (general form of if-then-else)
3 Alphabet declaration syntax is improved to support variables
4 special synbols are removed in assertion, key words are used for better parsing result and readability.
Bug fixing:
1 FD refinement checking is re-implemented. The previous version's implementation is not correct.
2 Corner cases improvement
Performance Improvement:
1 Self-implemented hashtable is used to replace built-in Dictionary in .NET. (both smaller and faster)
2 Code optimization round one is done. We are doing the round two now. :)
The user manual is available ''[[online|OnlineHelp/index.htm]]''.
The CHM version can be downloaded ''[[HERE|OnlineHelp/Help.chm]]''.
If you are interested in the technical details of PAT, refer to our [[Publications]].
1 A lot of bug fixing and performance improvement for PAT 1.2.6 are implmenented.
2 Search depth control is added to deadlock and reachability model checkers.
3 Parser improved and updated to the latest Antlr version.
4 New examples are added in. Examples are grouped in different categories.
5 Manual updated.
From now on, we will start PAT 2.0 development to support multi-languages.
PAT 2.0 is ready. In the new version, we did some structure changes to make the design more modulerize. The web service module is ready to use. We will stop the update of PAT 1.3.1. The latest version of CSP module is already integrated in the PAT 2.0.
!''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.
PAT has its own domain now: http://pat.comp.nus.edu.sg
The email address is "pat at comp dot nus dot edu dot sg", replace dot with '.'
Send an email to pat to join the mail list to get the update of PAT!
Note: due to the URL change, the auto update function will not working for the old version of PAT.
Please download the new version!
Sorry for the fast version update. :)
But we changed some syntax, which is big enough to make a new version.
Language Change:
1 use var to declare a variable, similar to javascript and ation script.
2 () is optional in process definition if there is no parameter.
Assertion:
State refinement //srefine// and //sequal// assertions is added into the system.
Optimization:
1 Self implemented hashtable and dictionary is used in the code.
2 Code tidy up.
User Manual:
[[User Manual|Help.htm]] is updated to the latest syntax.
!''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
In this release, we supported process level fairness and improve the performance and fix bugs. The parameterized verification (handling infinite number of threads) is under implementation now. We will release a new version soon once we have tested the programs.
Process level Fairness
Process level week and strong fairness is supported in PAT.
Performance Improvement
1 Strong Fairness Checking performance improvement
2 Refinement Checking speed-up.
3 Use Static variables
4 Fair-Loop checking is improved for the non-buchi-fair loops.
User Interface Simplification
1 Remove the tree data manager since the memory saving is not significant and memory is cheap now.
2 Fairness options are grouped into a combobox. The options are dynamically changed according to the applicablity.
New Examples:
1 Leader Election Protocols
2 Web Service: Travel Agent
3 Linearizability: SNZI Algorithms
Parser Library is updated to ANTLR 3.1.2
The beta version of PAT 2.0 is released with generic archetecture:
1 The lastest version of CSP module is integrated in PAT 2.0.
2 The newly developed web service module is implemented in PAT 2.0.
Go to [[Download]] to download it.
[[Process level fairness is supported: include global, strong and weak fairness]]
Leader Election protocol examples are implemented and built-in PAT.
These examples models an leader-election algorithm for graph/network rings using a leader detector. For details, refer to the paper "M. J. Fischer and H. Jiang. Self-stabilizing leader election in networks of finite-state anonymous agents. In Proc. 10th Conference on Principles of Distributed Systems, volume 4305 of LNCS, pages 395-409. Springer, 2006."
We have restructured the code to a better archetecture.
There is no function improvement.
!''What's new in PAT 2.3.0''
In this release, PAT supports several new language features to increase the expressiveness. Library support is improved to make it more useful. New examples are added. The details are explained as follows.
''Language Changes of CSP module''
1 Array can be passed in both synchronous and asynchronous channels
2 N-dimensional array is supported by converting them into one dimensional array in the parsing.
var matrix[N][10];
matrix[1][2] = 1;
3 Compound channel data are support. since FDR and SPIN support this. We adopted FDR's syntax
c?x.y.z or c!x.y.z
4 Array of size 0 is supported, you can use 0 size array as set of List with the help of C# library. See the library update below for more details.
''User Interface''
1 Bugs in model checking window are fixed.
2 Cut number display in the simulator is added if there is a one.
3 C# code library editor and compiler is improved.
''C# library support''
Users can create the external methods with int, bool or int array type parameters, with possible return type int, bool and int array. The number of parameters can be 0 to many now. PAT is abled to support multiple C# libraries. Currently two Libraries are implemented: Array and Set. More are coming. :)
6 User manual is updated, you can find info about all these update in the manual.
''Newly added examples''
a) Meta-Lock Example is added for the parameterized systems
b) Language feature demonstration example is added
Find them at [[User Manual]].
In the new version, we unified the denotation values of expression and expression class. In this way, the system is more simpler, there is no need to differenciate the value and expressions.
Negtive constant declaration is supported!
Bugs in the channel evaluation is fixed.
We would like to thank CS4211 students for the careful testings and feedbacks. Their efforts make PAT more stable!
Our paper [[Bounded Model Checking of Compositional Processes|http://www.comp.nus.edu.sg/~sunj/Publications/TASE2008.pdf]] is presented at 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008).
In this release, we have three main updates:
1 PAT 1.2.9 solves all the problems with Vista.
2 LTL2BA libary is completely rewritten using C#.
3 Bugs related to channels are fixed.
For the previous users, if you are using Windows Vista, please un-install the previous version of PAT and install PAT 1.2.9.
PAT 1.2.9 allows you to run PAT using administrative rights. You will not have any problems related to loading math library.
Parallel Model Checking for LTL properties are implemented.
If you are using Multi-core CPU, this feature allows you to speed-up the verification to several times.
UK
Germany
Singapore
Russia
France
Japan
China, Taiwan
China,
Egypt
China, Macao
Vietnam
Czech Republic
Australia
Denmark
India
Spain
USA
Canada
New Zealand
Brazil
Netherlands
Luxembourg
UK
Germany
Singapore
Russia
France
Japan
China, Taiwan
China,
Egypt
China, Macao
Vietnam
Czech Republic
Australia
Denmark
India
Spain
USA
Canada
New Zealand
Brazil
Netherland
Luxembourg
Colombia
''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.
PAT is presented in [[ICSE 2008|http://icse08.upb.de/]].
The presentation poster is here:
[img[PAT Poster|ICSE_Poster.jpg]]
In the early version, due to the difficulty of calculating alphabet of the process for parallel composition, PAT does not allow global variables in events or process invocations. But there are a lot of models needs this features.
In this release, we added the support of use of global variables in event and process invocation if there is no parallel composition involving. Runtime exceptions will be thrown if there is a difficult to calculate the alphabet due to usage of global varaibles.
We also add a single lift system example. Some examples are simplied after the new language feature.
Bugs fixing in simulator.
Optimizations are implemented as well for numerous places.
<html>
<body leftMargin=0 topMargin=0 marginheight="0" marginwidth="0">
<DIV
style="PADDING-BOTTOM: 10px; PADDING-LEFT: 10px; PADDING-RIGHT: 10px; PADDING-TOP: 10px"><FONT
face=Tahoma><FONT color=#800000 size=4></FONT> </FONT>
<P><FONT face=Arial><FONT size=2>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>PAT only
supports <STRONG>integer</STRONG>, <STRONG>Boolean </STRONG>and
<STRONG>integer arrays </STRONG>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
<EM>ExpressionValue</EM>.</FONT></SPAN></SPAN></FONT></SPAN></SPAN></FONT></P>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>The
following is one simple example showing how to create a hashtable
in C#.</FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>
<TABLE style="WIDTH: 687px; BORDER-COLLAPSE: collapse; HEIGHT: 1159px"
borderColor=#000000 cellSpacing=0 cellPadding=2 width=687 border=1>
<TBODY>
<TR>
<TD>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM>using System.Collections;<BR><FONT color=#0000ff>using
PAT.Common.Classes.Expressions.ExpressionClass;</FONT></EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM>//the namespace must be PAT.Lib, the class and method names can
be arbitrary<BR>namespace PAT.Lib {<BR> public class
HashTable : ExpressionValue
{<BR> public Hashtable
table;</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> /// Default
constructor without any parameter must be
implemented<BR> public <FONT
color=#0000ff>HashTable</FONT>()
{<BR>
table = new Hashtable();<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> public
HashTable(Hashtable newTable)
{<BR>
table = newTable;<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> public void Add(int
key, int value)
{<BR>
if(!table.ContainsKey(key))
{<BR>
table.Add(key,
value);<BR>
}<BR>
}<BR>
<BR> public bool ContainsKey(int
key)
{<BR>
return
table.ContainsKey(key);<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> public int
GetValue(int key)
{<BR>
return (int)table[key];<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> /// Return the
string representation of the hash
table.<BR> /// This method must
be overriden<BR> public override
string <FONT color=#0000ff>ToString</FONT>()
{<BR>
string returnString =
"";<BR>
foreach (DictionaryEntry entry in table)
{<BR>
returnString += entry.Key + "=" + entry.Value +
",";<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM>
return returnString;<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> /// Return a deep
clone of the hash table<BR> ///
This method must be
overriden<BR> public override
ExpressionValue <FONT color=#0000ff>GetClone</FONT>()
{<BR>
return new HashTable(new
Hashtable(table));<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> /// Return the
compact string representation of the hash
table.<BR> /// This method must
be overriden<BR> /// Smart
implementation of this method can reduce the state space and speedup
verification <BR> public
override string <FONT color=#0000ff>GetID</FONT>()
{<BR>
string returnString =
"";<BR>
foreach (DictionaryEntry entry in table)
{<BR>
returnString += entry.Key + "=" + entry.Value +
",";<BR>
}</EM></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM>
return returnString;<BR>
}<BR>
}<BR>}</EM></FONT></SPAN></SPAN></P></TD></TR></TBODY></TABLE></FONT></SPAN></SPAN></P>
<P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3></FONT></SPAN></SPAN></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><FONT
face=Arial size=2> </FONT><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>Note the
following requirements when you create your own data structure
objects:</FONT></SPAN></SPAN></SPAN></SPAN></FONT></P>
<UL>
<LI><FONT face=Arial></FONT><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>The
namespace must be "PAT.Lib", otherwise it will not be recognized. There is no
restriction for class names and method
names.</FONT></SPAN></SPAN></FONT>
<LI><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT color=#0000ff
size=3><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT color=#000000
size=3>Importing the PAT Expression name
space using "</FONT></SPAN></SPAN></SPAN></SPAN><EM>using
PAT.Common.Classes.Expressions.ExpressionClass;</EM><FONT color=#000000>".
</FONT></FONT></SPAN></SPAN></SPAN></SPAN></FONT></SPAN></SPAN></FONT>
<LI><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"></SPAN></SPAN></SPAN></SPAN>Only
public methods can be used in PAT models</FONT></SPAN></SPAN></FONT>
<LI><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"></SPAN></SPAN></FONT><FONT
face=Arial></FONT><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>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)</FONT>.</SPAN></SPAN></FONT>
<LI><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>The
number of parameters can be 0 or many.</FONT></SPAN></SPAN></FONT>
<LI><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"></SPAN></SPAN></FONT><FONT
size=3><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>The
return type must be of type "void", "bool", "int", "int[]" (int
array) or user defined data type</FONT>.</SPAN></SPAN></FONT>
<LI><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>The
method names are case sensitive.</FONT></SPAN></SPAN>
<LI><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>Put
the compiled dlls in "Lib" folder of the PAT installation directory to make
the linking easy by using <EM>#import
"DLL_Name";</EM></FONT></SPAN></SPAN></SPAN></SPAN></FONT></LI></UL></FONT></SPAN></SPAN>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>if your
methods need to handle exceptional cases, you can throw PAT runtime
exceptions as illustrated as the following example.</FONT></SPAN></SPAN> </P>
<P></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>
<TABLE style="WIDTH: 835px; BORDER-COLLAPSE: collapse; HEIGHT: 161px"
borderColor=#000000 cellSpacing=0 cellPadding=2 width=835 border=1>
<TBODY>
<TR>
<TD>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM>public static int StackPeek(int[] array)
{<BR> if (array.Length >
0)<BR> return
array[array.Length - 1];</EM></P>
<P><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT
size=3><EM> //throw PAT Runtime
exception<BR> throw new
PAT.Common.Classes.Expressions.ExpressionClass.RuntimeException("Access an
empty
stack!");<BR>}</EM></FONT></SPAN></SPAN></P></FONT></SPAN></SPAN></TD></TR></TBODY></TABLE></FONT></SPAN></SPAN></P></FONT></SPAN></SPAN></FONT><FONT
size=3><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>To
import the libraries in your model, users can using following
syntax:</FONT></SPAN></SPAN></SPAN></SPAN></FONT></SPAN></SPAN></SPAN></SPAN></FONT></P>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>#<FONT
color=#0000ff>import</FONT> "PAT.Lib.Hashtable"; <EM>//to import a library under
Lib folder of PAT installation path</EM><BR>#<FONT color=#0000ff>import</FONT>
"C:\Program Files\Intel\Hashtable.dll"; <EM>//to import a library using absolute
path</EM></FONT></SPAN></SPAN></SPAN></SPAN></FONT></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></FONT></SPAN></SPAN></SPAN></SPAN></FONT></P></FONT></SPAN></SPAN></FONT><FONT
size=3><SPAN style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>To
declar the user defined types in your models, please use the following
syntax</FONT>:</SPAN></SPAN></FONT></P>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3><FONT
color=#0000ff>var<</FONT>HashTable> table; <EM>//use the class name here
as the type of the varaible.
</EM></FONT></SPAN></SPAN></SPAN></SPAN></FONT></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></FONT></SPAN></SPAN></SPAN></SPAN></SPAN></SPAN></FONT></FONT></SPAN></SPAN></FONT></P>
<P><FONT size=3><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><SPAN
style="FONT-SIZE: 13.5pt; FONT-FAMILY: 'Arial Unicode MS'"><FONT size=3>To
invoke the public methods in your models, please use the
following syntax</FONT>:</SPAN></SPAN></FONT></P>
<UL>
<LI><FONT face="Arial Unicode MS" size=3>table.Add(10, 2); </FONT>
<LI><FONT size=3></FONT><FONT face="Arial Unicode MS"><FONT size=3><FONT
color=#0000ff>if</FONT>(table.ContainsKey(10))...</FONT>
</FONT></LI></UL></FONT><BR></FONT><FONT
color=#808080 size=2 face="Times New Roman"><FONT color=#808080 size=1
face=Arial>
<HR>
Copyright © 2007-2009 School of Computing, National University of
Singapore</FONT></FONT>
<P></P></DIV>
</html>
!''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.
!''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.
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/
The user manual is available ''[[online|OnlineHelp/index.htm]]''.
The CHM version can be downloaded ''[[HERE|OnlineHelp/Help.zip]]''.
If you are interested in the technical details of PAT, refer to our [[Publications]].
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 [[contact any one of us|About Us]].
Two big major update in PAT 1.2.2 are
1 MSAGL is integrated into PAT. We would like to thank Lev Nachmanson from Microsoft for his free offer of [[MSAGL: Microsoft Automatic Graph Layout|http://research.microsoft.com/research/msagl/]].
2 Auto-update function is added to PAT. Since we are doing some constant updating of the tool, it is annoying to send users email and do the installation again. Based on the ClickOnce, we have developed this custimized auto-update functions.
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|publications/fm09Counter.pdf]]''. The sixth International Symposium on Formal Methods (FM 2009). pages 123 - 139, Eindhoven, the Netherlands, November, 2009. ([[Slides|publications/fm09Counter.zip]])
* Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. ''[[Model Checking Lineariability via Refinement|publications/linearizability.pdf]]''. The sixth International Symposium on Formal Methods (FM 2009). pages 321-337, Eindhoven, the Netherlands, November, 2009. ([[Slides|publications/linearizability.ppt]])
If you are interested in software engineering and formal methods, you can contact us to plan your Final Year Project, Master or even Ph.D. relating to PAT. There are a lot of interesting research areas to explore and we also need good programers to make PAT more powerful and efficient.
For the details, check it out:
[[Add the syntax checking after parsing to rule out invalid/un-declared variables usage]]
[[Simulation window is redesigned completely]]
The PDF version of the PAT User Manual can be downloaded [[here|PATManual.pdf]]. We are keeping on working on a better version.
PAT 1.2.3 is released with the support of user defined math library. Also the c# math functions are supported. look [[Accept C# code as customized functions]] for details.
PAT project is initialized in School of Computing, National Univeristy of Singapore in July 2007. Our group is listed below.
The key members of PAT:
* Dr. [[SUN, Jun|http://www.comp.nus.edu.sg/~sunj]], Lee Kuan Yew Postdoc Fellow, School of Computing, National University of Singapore.
* Mr. [[LIU Yang|http://www.comp.nus.edu.sg/~liuyang]], PhD Candidate, School of Computing, National University of Singapore.
* Dr. [[DONG, JinSong|http://www.comp.nus.edu.sg/~dongjs/]], Associated Professor, School of Computing, National University of Singapore.
Students and Related Projects:
* Miss Zhang ShaoJie, PhD Candidate. Formal verification of UML.
* Miss Zheng Manchun, PhD Candidate. Formal verification of sensor network, particular NesC language.
* Mr Song SongZheng, PhD Candidate. Probabilistic model checking.
* Mr Tan Tian Huat, PhD Candidate, Model checking Web Services, currently working on Orc Module for PAT.
* Mr Luu Anh Tuan, PhD Candidate, Formal verification of security protocols.
* Mr Zhu Huiquan, PhD Candidate, Probabilistic model checking.
* Miss Shi Ling, PhD Candidate.
* Mr Cheng Bin, Undergraduate. PAT verification using Spec#
* Miss Zhao Wendi, Undergraduate. Transformation Promela (SPIN language) to CSP#
Should you meet any difficulty using PAT or find bugs of PAT or have some suggestion on improving PAT, please do not hesitate to contact any one of us. Alternatively, you can send an email to "pat at comp dot nus dot edu dot sg" (replace dot with '.').
!Acknowledgment
We own thanks to Truong Khanh (for solving the things for us), [[Jun Pang|http://satoss.uni.lu/members/jun/]] (for collabration on verifying population protocols), [[Hai Wang|http://users.ecs.soton.ac.uk/hw/]], [[Jing Sun|http://www.cs.auckland.ac.nz/~jingsun/]], [[Wei Chen|http://www.cs.sunysb.edu/~liu/]] and [[Annie Y. Liu|http://www.cs.sunysb.edu/~liu/]].
We are very grateful for the valuable comments and suggestions from professor [[Tony Hoare|http://research.microsoft.com/~thoare/]], professor [[Joxan Jaffar|http://www.comp.nus.edu.sg/~joxan/]], professor [[Jim Woodcock|http://www-users.cs.york.ac.uk/~jim/]], professor [[Jens Palsberg|http://www.cs.ucla.edu/~palsberg/]], professor [[Auguston Mikhail|http://faculty.nps.edu/maugusto/]], professor [[Kokichi FUTATSUGI|http://www.jaist.ac.jp/~kokichi]] and professor [[Kenji Taguchi|http://honiden-lab.ex.nii.ac.jp/~taguchi]] so on.
!Photos
The following is the picture of PAT group together with Turing Award winner [[Tony Hoare|http://research.microsoft.com/~thoare/]] (in center) in his visit to our lab in 2008.
<HTML>
<IMG SRC="./photos/group_photo.JPG" BORDER="0" ALT="">
</HTML>
To make the evaluation more efficient, we allow any math functions to be declared as static methods, which can be used directly in the model.
The static varaibles are be used as well.
To edit the math library code, click "Tools" -> "Math Library".
for example, if you declare the following static methods in math library code.
public static int max(int a, int b)
{
if(a > b)
return a;
else
return b;
}
In your model, you can use max as a function like following:
a = 0;
b = 15;
P() = event{a = call(max, 10, b);} -> Skip;
Also the full set C# math library can be used directly in the model:
Method Returns
Abs Returns the absolute value of a number.
Ceiling Returns a value that is the smallest whole number greater than or equal to a given number.
Exp Returns E raised to a given power. This is the inverse of Log.
Floor Returns a value that is the largest whole number that is less than or equal to the given number.
IEEERemainder Returns the result of a division of two specified numbers. (This division operation conforms to the remainder operation stated within Section 5.1 of ANSI/IEEE Std.
The parser is completely re-designed. Now the AST is built up and parsed using two time parsing process.
The two time parsing make it much easier to detect the un-declared variables and duplicated definitions.
The improvements are:
1 Constants can be declared at any place of the specification.
2 Un-declared variables and channel names are not allowed. Record variables are different from normal variables.
3 Same name is not allowed for different constants, global variables, channels names, LTL propersition names, and process names.
4 Constants, global variables, channels names, LTL propersition names, and process names are not allowed to be used as events names.
<<option chkGenerateAnRssFeed>> GenerateAnRssFeed
<<option chkOpenInNewWindow>> OpenLinksInNewWindow
<<option chkSaveEmptyTemplate>> SaveEmptyTemplate
<<option chkToggleLinks>> Clicking on links to tiddlers that are already open causes them to close
^^(override with Control or other modifier key)^^
<<option chkHttpReadOnly>> HideEditingFeatures when viewed over HTTP
<<option chkForceMinorUpdate>> Treat edits as MinorChanges by preserving date and time
^^(override with Shift key when clicking 'done' or by pressing Ctrl-Shift-Enter^^
<<option chkConfirmDelete>> ConfirmBeforeDeleting
Maximum number of lines in a tiddler edit box: <<option txtMaxEditRows>>
Folder name for backup files: <<option txtBackupFolder>>
<<option chkInsertTabs>> Use tab key to insert tab characters instead of jumping to next field
<HTML>
<HEAD>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
</HEAD>
<P>The Algorithms for the feasible test are shown as follows.</P>
<CENTER>
<IMG SRC="algo1.JPG" BORDER="0" ALT="">
</CENTER>
<P>The Algorithm for model checking is shown as follows.</P>
<CENTER>
<IMG SRC="algo2.JPG" BORDER="0" ALT="">
</CENTER>
</HTML>
CSP simulator takes in the specifications and allows users to perform various simulation tasks:
*Complete states generation based on the execution graph. The generation may not terminate if the states are not finite.
*Automatically Random Simulation with animation
*User interactive simulation with Step by Step execution
*Trace display and replay
A veriaty of systems have been analysized using PAT. Also, we have built-in some of the examples (with model description and user options) for user convenience. More may be expected in the future. You can also find more experiments in our [[publications|Publications]].
* newly developed population protocols, e.g., self-stablizing leader protocols for complete network, network rings, rooted tree, etc.
* the [[pace maker|http://sqrl.mcmaster.ca/pacemaker_spec.htm]] system from the [[pace maker challenge|http://sqrl.mcmaster.ca/pacemaker.htm]].
* security protocols, e.g., multi-party contract signing protocol.
* concurrent algorithms, e.g., concurrent stack, queue, the mailbox problem, etc.
* real applications: lift system, keyless car system.
* benchmark systems like dining philosophers, Milner's cyclic scheduler, Peterson's algorithm, etc.
!Experiments of Leader Election Protocols with fairness
The following are some experiment results obtained using PAT version 1.3.0. As we are actively developing PAT, the number may not be exact now. The data is obtained on Windows XP platform with Core 2 CPU 6600 at 2.4 GHZ and 2GB Memory. It shows the verification statistics over recent population protocols, namely self stablizing leader election for complete networks, for rooted trees, for odd sized rings, for network rings and token circulation for network rings. Correctness of all these examples relies on some form of fairness.
<HTML>
<CENTER>
<IMG SRC="./performance1.jpg" BORDER="0" ALT="">
</CENTER>
</HTML>
!Experiments of fairness properties and comparson with SPIN
The following shows verification statistics of benchmark systems to show other aspects of PAT. Because of the deadlock state, the dining philosophers model (dp(N) for N philosophers and forks) does not guarantee that a philosopher always eventually eats ([]<> eat0) whether under no fairness or the strongest fairness. This experiment shows \textsc{Pat} takes little extra time for handling the fairness assumption. Notice that SPIN finds a counterexample (under no fairness) quickly. This is due to the particular order of exploration as well as its nested depth-first-search algorithm. Milner's cyclic scheduler algorithm (ms(N) for N processes) is a showcase for the effectiveness of partial order reduction. We apply fairness in two different ways, i.e., one applying strong local fairness to the whole system (slf-whole) and the other applying only to inter-process communications (slf-action). In the latter case, partial order reduction allows us to prove the property over a much larger number of processes (e.g., 200 vs 12). Peterson's mutual exclusive algorithm (peterson(N)) requires process-level weak fairness to guarantee bounded by-pass. The property is verified under weak fairness in PAT and process-level weak fairness in SPIN. PAT outperforms SPIN in this setting.
<HTML>
<CENTER>
<IMG SRC="./performance2.png" BORDER="0" ALT="">
</CENTER>
</HTML>
!Experiments of linearizability and refinement checking
Experiment results of PAT 1.2.6 build 4600 on linearizability testing based on the refinement relations are shown in the following figure. The testbed is a PC with 2.83GHz Intel Core Quad Q9550 CPU and 4 GB memory.
<HTML>
<CENTER>
<IMG SRC="./performance3.png" BORDER="0" ALT="">
</CENTER>
</HTML>
In the experiments, the number of states and the running time increase rapidly with increasing data size or the number of processes, e.g., 3 processes (in the Register , Stack or Queue) vs. 2 processes. Nonetheless, because of partial order reduction (as well as other built-in optimization techniques), our algorithm is more robust to the data size. The partial order reduction can effectively reduce the search space and running time in most of the cases (Mailbox, Stack, Queue). However, in Register , partial order reduction produces fewer states but bigger normalized states, which increases running time when the number of states increases. The counterexamples in the Buggy Queue are detected quickly by searching part of the state space. Compared with the results in other method, our solution is much more scalable to handle all the possible interleaving of operations. In summary, PAT is effective and can handle millions of states in hours.
* Line Number Display.
* Syntax Highlight with Configuration File.
* Multi Documents Working Enviroment.
* Various Shortcuts Editing Function.
Since PAT is still in the beta version stage, it is important to use unit testing to make sure the new changes will not distroy correstness of the old functions. We adopted [[nunit|www.nunit.org]] as the unit testing tool. Hopefully, we can complete the unit testing to catch up the latest development.
The [[dining philosophers|http://en.wikipedia.org/wiki/Dining_philosophers_problem]] problem is summarized as five philosophers sitting at a table doing one of two things - eating or thinking. While eating, they are not thinking, and while thinking, they are not eating. The five philosophers sit at a circular table with a large bowl of spaghetti in the center. A fork is placed in between each philosopher, and as such, each philosopher has one fork to his or her left and one fork to his or her right. As spaghetti is difficult to serve and eat with a single fork, it is assumed that a philosopher must eat with two forks. The philosopher can only use the fork on his or her immediate left or right.
The CSP Definition of Dining Philosophers:
<HTML>
<HEAD>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
</HEAD>
<CENTER>
<IMG SRC="dp.JPG" BORDER="0" ALT="">
</CENTER>
</HTML>
The property interested states that every philosopher will always eventually eat, i.e., no one shall starve.
<HTML>
<HEAD>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
</HEAD>
<CENTER>
<IMG SRC="dpltl.JPG" BORDER="0" ALT="">
</CENTER>
</HTML>
The following defintion is the Dining Philosophers example with size 3.
//====================Process Definitions====================
phi0()=((t0->phi0())[](wl(g01)->(g00->(e0->(p01->(p00->phi0()))))));
f0()=((g00->(wl(p00)->f0()))[](g20->(wl(p20)->f0())));
phi1()=((t1->phi1())[](wl(g12)->(g11->(e1->(p12->(p11->phi1()))))));
f1()=((g11->(wl(p11)->f1()))[](g01->(wl(p01)->f1())));
phi2()=((t2->phi2())[](wl(g20)->(g22->(e2->(p20->(p22->phi2()))))));
f2()=((g22->(wl(p22)->f2()))[](g12->(wl(p12)->f2())));
DiningPhilosophers()=(phi0()||f0()||phi1()||f1()||phi2()||f2());
//============================Assertions===========================
#assert DiningPhilosophers() |= []<>e0;
#assert DiningPhilosophers() deadlockfree;
#assert DiningPhilosophers() feasible;
#assert DiningPhilosophers() |= []<>e0 && []<>e1 && []<>e2;
We found a bug in ListView Control of .NET Framework for the forecolor and backcolor display of sub-items.
The following code samples provide the solution to fix them.
ListView_EnabledEvents.OwnerDraw = true;
ListView_EnabledEvents.DrawItem += new DrawListViewItemEventHandler(ListView_EnabledEvents_DrawItem);
ListView_EnabledEvents.DrawColumnHeader += new DrawListViewColumnHeaderEventHandler(ListView_EnabledEvents_DrawColumnHeader);
private void ListView_EnabledEvents_DrawColumnHeader(object sender, DrawListViewColumnHeaderEventArgs e)
{
e.Graphics.FillRectangle(Brushes.GreenYellow, e.Bounds);
e.DrawText();
e.DrawDefault = true;
}
private void ListView_EnabledEvents_DrawItem(object sender, DrawListViewItemEventArgs e)
{
Rectangle foo = e.Bounds;
foo.Offset(-10, 0);
e.Graphics.FillRectangle(new SolidBrush(e.Item.BackColor), foo);
e.DrawDefault = true;
}
Latest version PAT 2.7.0 includes the stable version of the CSP module and a beta version of Real-Time System Module and the Web Service module.
Click [[HERE|http://patroot.com/register/register.php]] to download. If you experience difficulty downloading, do send me an [[email|About Us]] and we shall contact you as soon as possible (within the same day).
Please See [[Version History]] for the detailed history.
If you are interested in obtaining the source code of PAT, please contact any one of the authors or send us [[email|About Us]]. Recently, GLEE is commerialized and renamed to [[MSAGL: Microsoft Automatic Graph Layout|http://research.microsoft.com/research/msagl/]]. Since we used MSAGL and it becomes difficult to distribute the source code. Therefore, only old version of PAT, which uses GLEE, is available upon request.
!''System Requirement''
* Windows Operating System: Windows XP, Vista and Windows Server 2000/2003. PAT is developed for Windows platform.
* .NET Framework 2.0 (.NET Framework 3.5 is the lastest) is needed to run PAT, which can be downloaded [[here|http://www.microsoft.com/downloads/details.aspx?familyid=0856EACB-4362-4B0D-8EDD-AAB15C5E04F5&displaylang=en]].
!''Installation''
Installing PAT is easy: run the setup file and follow the installation wizard. The following are the system requirements.
!Note for Vista users: starting from version 1.2.9, PAT can run smoothly with UAC enabled. Please un-install the previous version of PAT, and install 1.2.9 if you are using Vista. Otherwise, the UAC problem will be still there and you can not load the math library.
!Note: If you have problem to start the Simulator, please download the [[DLL|System.Core.dll]] and put it under your installation folder.
![[PAT Installation FAQ]]
!''News''
* [[4, Nov, 2009: PAT is presented FM 09]]
* [[24, Oct, 2009: Warning List is supported. PAT makes the modeling easier!]]
* [[30, Sep, 2009: PAT Japanese user group formed]]
* [[25, Sep, 2009: PAT supports user defined data structures]]
* [[05, Sep, 2009: PAT 2.7.0 is released!]]
* 29, Jul, 2009: PAT is presented CAV 09 and TASE 09
* [[09, Jun, 2009: PAT 2.6.0 is released!]]
* [[02, Jun, 2009: PAT 2.5.0 is released!]]
* [[30, Apr, 2009: http://www.patroot.com is online]]
* [[30, Apr, 2009: PAT 2.4.0 is released!]]
* [[13, Apr, 2009: PAT 2.3.0 is released!]]
* [[Old News]]
!''Introduction''
Critical system requirements like safety, liveness and fairness play important roles in software specification, development and testing. It is desirable to have handy tools to simulate the system behaviors and verify critical properties. Process Analysis Toolkit (also known as PAT, [[Screen Shots|Screen Shots]]) was initially design to investigate system (specified using the classic process algebra Communicating Sequential Processes - CSP) verification under fairness assumptions. The motivation is that fairness assumptions are often necessary in system verification practice in order to prove desirable system properties, whereas existing languages and tools have limited support for fairness modeling as well as verification. We have successfully demonstrated PAT as an analyzer for extended process algebras at ICSE 2008. Since then, PAT has been evolved to be a self-contained framework to support concurrent system analysis. So far, PAT has attracted ''350'' downloads from ''93'' organizations in ''[[23 countries and regions]]''.
Starting from PAT 2.0, we applied a a modularized design to support the analysis of the different system/languages. Each language is encapsulated as one module with predefined APIs, which identify the (specialized) language syntax, well-formness rules as well as (operational) formal semantics, and loaded at run time according to the input model. This architecture allows new languages to be developed easily by providing the syntax rules and semantics. Till now, two modules have been developed, namely Communicating Sequential Processes (CSP) module and Web Service (WS) module. In the future, our targeted systems include security domain (security protocals), UML (state chart and sequence diagrams), real time systems and so on.
*''CSP Module''
The input language of CSP module supports high-level compositional constructs like (de-terministic/non-deterministic) choice, parallel, interleaving, interrupt, etc, as well as low-level programming language constructs like shared variables, arrays, if-then-else, etc. A user-friendly simulator is designed to animate system behaviors interactively. More importantly, complementing model checking algorithms have been implemented to assist analysis of concurrent systems. PAT supports standard reachability analysis, deadlock checking, refinement checking and verification of LTL formulae. Distinguished from existing model checkers, PAT found its strength in two unique aspects. Firstly, it is designed to verify systems under a variety of fairness assumptions, e.g., weak fairness, strong local/global fairness, etc. Secondly, it supports mechanical refinement checking (with data refinement relationships), which makes the verification of some critical properties in distributed algorithms (e.g., linearizability) possible. In order to handle large systems, PAT is further improved with effective reduction techniques like partial order reduction. PAT has been applied to a number (still growing) of real world problems, ranging from benchmark systems, recently population/security protocols and distributed algorithms. Previously unknown bugs have been discovered. Our experiments show that PAT is capable of handling systems with large number of states (refer to [[experiments|Case Studies]]) and complements existing state-of-the-art model checkers (e.g., SPIN and FDR) in a number of aspects. The following are the main functionalities of PAT.
* User friendly editing environment (with advanced syntax editing features) for introducing CSP models, CSP models extended with shared variables/arrays, asynchronous communication channels, event-based fairness, State/Event LTL and other features.
* User friendly simulator for interactively and visually simulating system behaviors; by either random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
* Click button model checker for deadlock-freeness verification, reachability analysis, state/event linear temporal logic verification (with or with fairness) and refinement checking.
* A wide range of built-in examples ranging from benchmark systems to newly developed algorithms/protocols.
PAT is distinguished in a number aspects from existing model checkers. In the following, we briefly introduce the two of them. To reveal the full details, please refer to our [[publications|Publications]] (some of yet to be published and therefore will be available later).
The LTL model checking algorithm in PAT is designed to handle a variety of fairness constraints efficiently. This is partly motivated by recently developed population protocols, which only work under weak, strong local/global fairness. The other motivation is that the current practice of verification is deficient under fairness. Two different approaches for verification under fairness are supported in PAT, targeting different users. For ordinary users, one of the following options may be chosen and applied to the whole system: weak fairness or strong local/global fairness. The model checking algorithm works by identifying the fair execution at a time and checks whether the desirable property is satisfied. Notice that unfair executions are considered unrealistic and therefore are not considered as counterexamples. Because of the fairness, nested depth-first-search is not feasible and therefore the algorithm is based on an improved version of Tarjan's algorithm for identifying strongly connected components. We have successfully applied it to prove or disprove (with a counterexample) a range of systems where fairness is essential. In general, however, system level fairness may sometimes be overwhelming. The worst case complexity is high and, worse, partial order reduction is not feasible for model checking under strong local/global fairness. A typical scenario for network protocols is that fairness constraints are associated with only messaging but not local actions. We thus support an alternative approach, which allows users annotate individual actions with fairness. Notice that this option is only for advanced users who know exactly which part of the system needs fairness constraints. Nevertheless this approach is much more flexible, i.e., different parts of the system may have different fairness. Furthermore, it allows partial order reduction over actions which are irrelevant to the fairness constraints, which allows us to handle much large systems.
LTL formulas assert properties over each and every single executions of the system, PAT allows users to reason about behaviors of a system as a whole by refinement checking. Refinement checking is to verify whether an implementation's behaviors follow the specifications. PAT supports six notions of refinements based on different semantics, namely trace refinement, stable failures refinement, failures divergence refinement and each of the above refinement augmented with data refinement. A refinement checking algorithm (inspired by the one implemented in FDR but extended with partial order reduction) is used to perform refinement checking on-the-fly. Refinement checking in FDR only compares the traces (e.g., event sequences) of the implementation and the specification. For practical systems (other than those specified with process algebras), it may be desirable to also compare the data structures. For instance, linearizability is an important correctness criteria for concurrent data structure. Informally, it requires that the data structure accessed by multiple processes concurrently must be updated as if the processes access it sequentially. To establish a refinement relationship, not only the event of accessing the data structure must be compared between a sequential specification and a concurrent implementation, but also the data structure itself must be checked. We thus provide a user option to state whether to check for data refinement.
*''Real-Time System Module''
Real-time system module supports 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, within, 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.
*''Web Service Module''
Web service is an emerging area with promising applications as well as unique challengers on system analysis. The WS module is designed to systematically solve two important problems on web services design and realization. One is how to verify whether the web services are correct, either by showing that orchestration of the web services satisfies user-specified temporal properties or by showing that the orchestration conforms to a given choreography. The other is how to automatically synthesize an orchestration of Web services from a given choreography. The verification problem is solved by adopting and improving existing reachability analysis and refinement checking algorithms in PAT. A lightweight yet effective method is developed to solve the synthesis problem.
LTL - linear time temporal logic formulae for specifying correctness requirements.
SYNTAX
Grammar:
ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
Operands (opd):
true, false, and user-defined names starting with a ''lower-case letter''.
Unary Operators (unop):
[] or G (the temporal operator always)
<> or F (the temporal operator eventually)
! (the boolean operator for negation)
X (next)
Binary Operators (binop):
U (the temporal operator strong until)
V or R (release: the dual of U): (p V q) means !(!p U !q))
&& (the boolean operator for logical and)
|| (the boolean operator for logical or)
/\ (alternative form of &&)
\/ (alternative form of ||)
-> (the boolean operator for logical implication)
<-> (the boolean operator for logical equivalence)
DESCRIPTION
Our tool will translate LTL formulae into never claims automatically. So you do not need to write the negation for the property to be checked. The never claim that is generated encodes the Buchi acceptance conditions from the LTL formula. Formally, any omega-run that satisfies the LTL formula is guaranteed to correspond to an accepting run of the never claim.
All binary operators are left-associative. Parentheses can be used to override this default. Note that implication and equivalence are not temporal but logical operators.
EXAMPLES
[] p
''!''( <> !q )
p U q
p U ([] (q U r))
This document presents the EBNF syntax of the specifica tion language used in our model checker. The name vCSP stands for variables enriched Communicating Sequential Processes.
!''SYNTAX''
NOTE: the rules for expression and definition are written using a hierarchical order to show the precedences between these rules.
//the starting rule for the specification//
specification : specBody*;
specBody : letDefintion //global definitions//
| definition //process definitions//
| assertion //assertion definitions//
| alpha //alphabets definitions//
| define //global constants and condition declarations//
| channel //global channel declarations//
;
//various assertion definitions//
assertion : '#' 'assert' definitionRef
(
( '|=' ( '(' | ')' | '[]' | '<>' | ID | '!' | '&&' | '||' | '->' | '<->' | '/\\' | '\/' | '.' | INT )+ ) //LTL checking//
| 'deadlockfree' //deadlock testing//
| 'feasible' //feasibility testing//
| 'reachable' ID //reachability testing//
| '=T=' definitionRef //trace equivalence//
| '=F=' definitionRef //falure equivalence//
| '=FD=' definitionRef //falure divergence equivalence//
| '[T=' definitionRef //trace refinement//
| '[F=' definitionRef //falure refinement//
| '[FD=' definitionRef //falure divergence refinement//
)
';'
;
definitionRef : ID actualParameterList;
//alphabets definitions for CSP processes//
alpha : 'alpha' '(' ID ')' '=' '{' eventName (',' eventName )* '}' ';' ;
define : '#' 'define' ID INT ';' //global Int constant declaration//
| '#' 'define' ID ('true' | 'false') ';' //global Boolean constant declaration//
| '#' 'define' ID conditionalOrExpression ';'//global condition declaration, used in assertions//
;
//global channel declarations//
channel : 'channel' ID additiveExpression;
//statement expression//
statement : block
| funExpression
| recfunExpression
| applicationExpression
| ifExpression
| whileExpression
| letExpression
| expression ';'!
| ';'!
;
block : '{' statement+ '}' ;
funExpression : 'fun' notEmptyIdentifierList '->' statement ;
notEmptyIdentifierList : '(' ID (',' ID)* ')';
recfunExpression :'recfun' ID notEmptyIdentifierList '->' statement;
applicationExpression : '(' expression notEmptyExpressionList ')' ;
notEmptyExpressionList : expression+ ;
ifExpression : 'if' '(' expression ')' s1=statement ('else' s2=statement)? ;
whileExpression : 'while' '(' expression '}' statement ;
recordExpression : '[' expression (',' expression)* ']' ;
letExpression : 'let' letDefintion+ 'in' expression;
letDefintion : ID '=' expression ';'
| ID '=' recordExpression ';'
| ID '=' funExpression ';'
| ID '=' recfunExpression ';'
| ID'[' expression ']' ';' //integer array with initial values 0//
;
expression : conditionalOrExpression ('=' expression)? ;
conditionalOrExpression : conditionalAndExpression ( '||' conditionalAndExpression )* ;
conditionalAndExpression : equalityExpression ( '&&' equalityExpression)* ;
equalityExpression : relationalExpression ( ('==' |'!=') relationalExpression)* ;
relationalExpression : additiveExpression ( ('<' | '>' | '<=' | '>=') additiveExpression)* ;
additiveExpression : multiplicativeExpression ( ('+' | '-') multiplicativeExpression)* ;
multiplicativeExpression : unaryExpression ( ('*' | '/' | '%' ) unaryExpression)* ;
unaryExpression : '+' unaryExpression
| '-' unaryExpression
| unaryExpressionNotPlusMinus
;
unaryExpressionNotPlusMinus
: ID ('[' conditionalOrExpression ']')?
| INT
| 'true'
| 'false'
| '(' conditionalOrExpression ')'
| '!' conditionalOrExpression //negation
;
//CSP process definition
definition : ID formalParameters '=' ifExpr ';' ;
formalParameters : '(' (ID (',' ID )*)? ')' ;
ifExpr : 'if' (ifExprCondition+ ('else' ifExpr)? ) 'fi'
| interleaveExpr
;
ifExprCondition : (conditionalOrExpression ':' ifExpr);
interleaveExpr : parallelExpr ('|||' parallelExpr)*
| '|||' (paralDef (';' paralDef )*) '@' ifExpr
;
parallelExpr : internalChoiceExpr ('||' internalChoiceExpr)*
| '||' (paralDef (';' paralDef )*) '@' ifExpr
;
paralDef : ID ':' '{' additiveExpression (',' additiveExpression)* '}'
| ID ':' '{' additiveExpression '..' additiveExpression '}'
;
internalChoiceExpr : conditionalChoiceExpr ('<>' conditionalChoiceExpr)*;
conditionalChoiceExpr : externalChoiceExpr ( << conditionalOrExpression >> externalChoiceExpr)* ;
externalChoiceExpr : interruptExpr ('[]' interruptExpr)* ;
interruptExpr : hidingExpr ('|>' hidingExpr)*;
hidingExpr : sequentialExpr ('\\' '{' eventM (',' eventM )* '}')? ;
sequentialExpr : guardExpr (';' guardExpr)*;
guardExpr : channelExpr
| '[' conditionalOrExpression ']' '@' channelExpr
;
channelExpr : ('wl' | 'sl' | 'sf' | 'wf') '(' ID '!' expression ')' '->' eventExpr
| ('wl' | 'sl' | 'sf' | 'wf') '(' ID '?' ID ')' '->' eventExpr
| ID '!' expression '->' eventExpr
| ID '?' ID '->' eventExpr
| eventExpr
;
eventExpr : eventM (block)? '->' eventExpr
| atom
;
atom : ID actualParameterList
| 'Skip' ('(' ')')?
| 'Stop' ('(' ')')?
| '(' ifExpr ')'
;
actualParameterList : '(' (expression (',' expression )*)? ')' ;
eventM : eventName
| ('wl'|'sl'|'wf'|'sf') '(' eventName ')'
;
eventName : ID ( '.' additiveExpression)* ;
ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')* ;
INT : ('0'..'9')+ ;
COMMENT : '/*' TEXT '*/' ;
LINE_COMMENT : '//' TEXT '\r'? '\n';
!''OPERATOR PRECEDENCE''
The operators at the top of the table bind more tightly than those lower down.
<html>
<TABLE>
<TR><TD><B>Class</B>
<TD><B>Operators</B>
<TD><B>Description</B>
<TD><B>Associativity</B>
<TR><TD COLSPAN=4><HR NOSHADE>
<TR><TD>Sequential
<TD><TT>-></TT>
<TD>prefix
<TD>right
<TR><TD>
<TD><TT>;</TT>
<TD>sequence
<TD>left
<TR><TD COLSPAN=4><HR NOSHADE>
<TR><TD>Hiding
<TD><TT>\</TT>
<TD>hiding
<TD>-
<TR><TD COLSPAN=4><HR NOSHADE>
<TR><TD>Choice
<TD><TT>|></TT>
<TD>interrupt
<TD>left
<TR><TD>
<TD><TT>[]</TT>
<TD>external choice
<TD>left
<TR><TD>
<TD><TT><b></TT>
<TD>external choice
<TD>left
<TR><TD>
<TD><TT><></TT>
<TD>internal choice
<TD>left
<TR><TD COLSPAN=4><HR NOSHADE>
<TR><TD>Parallel
<TD><TT>||</TT>
<TD>parallel
<TD>left
<TR><TD>
<TD><TT>|||</TT>
<TD>interleave
<TD>left
</TABLE>
</html>
!''EXAMPLES''
The spefication of two Dining Philoshpors:
phi0()=((t0->phi0())[](wl(g01)->(g00->(e0->(p01->(p00->phi0()))))));
f0()=((g00->(wl(p00)->f0()))[](g10->(wl(p10)->f0())));
phi1()=((t1->phi1())[](wl(g10)->(g11->(e1->(p10->(p11->phi1()))))));
f1()=((g11->(wl(p11)->f1()))[](g01->(wl(p01)->f1())));
DiningPhilosophers()=(phi0()||f0()||phi1()||f1());
Type the text for 'InterfaceOptions'
By following [[Aaron Stebner's WebLog|http://blogs.msdn.com/astebner/archive/2006/08/12/696833.aspx]], we allow user to launch PAT after installation. We have updated the script to make it better.
* Download this [[script|EnableLaunchApplication.js]].
* To include this script as a post-build step in a Visual Studio setup/deployment project, you can use the following steps:
0 Download the sample script and extract the contents to the directory that contains the Visual Studio setup project you are working on.
Note: You should end up with the file EnableLaunchApplication.js in the same directory as the .vdproj file for your setup project. The rest of these steps will not work correctly if you do not put EnableLaunchApplication.js in the correct location, so be careful about this step.
1 Open the file EnableLaunchApplication.js in a text editor such as notepad, locate the variable at the top of the file that is set to the value WindowsApplication1.exe, and change it to the name of the EXE that is in your setup that you want to launch when the MSI is done installing
2 Open the project in Visual Studio
3 Press F4 to display the Properties window
4 Click on the name of your setup/deployment project in the Solution Explorer
5 Click on the PostBuildEvent item in the Properties window to cause a button labeled "..." to appear
6 Click on the "..." button to display the Post-build Event Command Line dialog
7 Copy and paste the following command line into the Post-build event command line text box:
cscript.exe "$(ProjectDir)EnableLaunchApplication.js" "$(BuiltOuputPath)"
8 Save your project, Build your project in Visual Studio
[[Home]]
[[System Design]]
[[Road Map]]
[[Download]]
[[User Manual]]
[[Case Studies]]
[[Publications]]
[[Version History]]
[[About Us]]
© 2007 - 2009
[[SoC, NUS|http://www.comp.nus.edu.sg]]
<html>
<a target="_blank" href="/cgi-bin/pagecount?/~pat/index.html">SOC Stats</a>
</html>
<html>
<a href="http://www2.clustrmaps.com/counter/maps.php?url=http://www.comp.nus.edu.sg/~pat" target="_blank" id="clustrMapsLink"><img src="http://www2.clustrmaps.com/counter/index2.php?url=http://www.comp.nus.edu.sg/~pat" style="border:0px;" alt="Locations of visitors to this page" title="Locations of visitors to this page" id="clustrMapsImg" onerror="this.onerror=null; this.src='http://clustrmaps.com/images/clustrmaps-back-soon.jpg'; document.getElementById('clustrMapsLink').href='http://clustrmaps.com';" />
</a>
</html>
<HTML>
<HEAD>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
</HEAD>
<CENTER>
<IMG SRC="ms.JPG" BORDER="0" ALT="">
</CENTER>
</HTML>
The property to verify is that a process must eventually be scheduled.
//[]<>work0//
The following defintion is the MS example with size 3.
====================Process Definitions====================
//start()=(bang->Stop);
cycle0()=((bang->(a.0->((work0->(init.1->cycle0))[](init.1->(work0->cycle0)))))
[](init.0->(a.0->((work0->(init.1->cycle0))[](init.1->(work0->cycle0))))));
cycle1()=(init.1->(a.1->((work1->(init.2->cycle1))[](init.2->(work1->cycle1)))));
cycle2()=(init.2->(a.2->((work2->(init.0->cycle2))[](init.0->(work2->cycle2)))));
aMilnerScheduler()=(start||cycle0||cycle1||cycle2);
//
====================LTL Definitions========================
//LTL(AlwaysWork0=[]<>work0);
//
We have implemented both explicit model checking as well as bounded model checking for systematic analysis of CSP models. In our implementation, there is 2 model checkers are implemented:
* [[On-the-fly model checking||http://www.comp.nus.edu.sg/~liuyang/veri]]: to verify the CSP processes with or without fair events.
* Bounded model checking: to verify the CSP processes without fair events based on the SAT Solvers.
The details of the two model checkers are in the submitted publications.
* [[30, Mar, 2009: PAT 2.2 User Manual is online!]]
* [[27, Mar, 2009: PAT 2.2.0 is released!]]
* [[09, Mar, 2009: PAT 2.1.0 is released!]]
* [[05, Jan, 2009: PAT 2.0 is released!]]
* [[21, Dec, 2008: PAT 1.3.1 is released!]]
* [[10, Dec, 2008: PAT 2.0 Beta is released!]]
* [[04, Dec, 2008: PAT User Manual is online!]]
* [[25, Nov, 2008: PAT 1.3.0 is released!]]
* [[19, Nov, 2008: PAT 1.2.9 is released! Please re-install PAT!]]
* [[15, Nov, 2008: PAT 1.2.8 is released!]]
* [[04, Nov, 2008: PAT 1.2.7 is released!]]
* [[13, Oct, 2008: PAT tutorials and lecture notes are added]]
* [[06, Oct, 2008: New URL and PAT MailList]]
* [[06, Oct, 2008: PAT 1.2.6 is released!]]
* [[03, Oct, 2008: PAT 1.2.5 is released!]]
* [[11, Sep, 2008: PAT 1.2.4 is released!]]
* [[8, Aug, 2008: PAT 1.2.3 is released!]]
* [[6, Aug, 2008: PAT User Manual is updated]]
* [[31, July, 2008: PAT 1.2.2 is released!]]
* [[10, July, 2008: PAT 1.2.0 is released!]]
* [[17, June, 2008: PAT is presented in TASE 2008]]
* [[25, May, 2008: PAT is presented in ICSE 2008]]
* [[5, May, 2008: The PAT's User Interface and Language Parser are completely redesigned.]]
* [[5, May, 2008: PAT wants You!]]
!1 I can not install PAT.
Answer:
a) Make sure you have install the .NET framework 2.0.
b) Make sure the installation file is correctedly downloaded: "PAT.Setup.XXX.msi". Some users accidentally rename the installation file with extra .exe in the end.
c) The last remedy is to download direct executable of PAT and run it directly without installation
!2 Can I run PAT in linux or Solaris, Mac OS X and Unix?
Answer:
Currently, it is not that easy. One solution for Mac OS is to use virtual PC like [[parallel|http://www.parallels.com]] to install windows, or install windows using BootCamp.
For other OS, we are trying to use [[Mono|http://www.mono-project.com/Main_Page]] to achieve this goal, but it has some problems currently.
!3 I can not start the simulator.
Answer:
Please make sure you have [[this DLL|System.Core.dll]] under your installation folder.
In this section, we present the performance study of PAT. Note that we are actively profiling and fine-tuning PAT and thus the experiment results may vary day-to-day. The classification of the examples can be obtained from this [[document|result.doc]].
* [[Performance comparison with SPIN and FDR for Model Checking]]
* [[Performance Study for Model Checking Optimization Techniques]]
* [[Performance Study for Refinement Checking]]
* [[Performance Study of Leader Election Protocols]]
The following table presents part of the experimental results of PAT (conducted on Windows XP with a 2.0 GHz Intel Core Duo CPU and 1 GB memory). The first model is the dining philosophers. The property is []<>eat.0. Without fairness assumptions, this property is false. A counterexample is quickly produced in most of the cases. Nonetheless, it may take considerably long if the trace leading to a counterexample is explored very late (e.g., for College(15) without reduction). Partial order reduction significantly reduces the time to discover a counterexample for this example. This model is then annotated with fairness. The last three columns show verification results of lCollege(N). The property becomes true and therefore a complete search is necessary. Note that partial order reduction gains little. The reason is that the model is highly coupled and heavy in communication. Manually hiding local communicating could reduce the verification time. The second model is Milner’s cyclic scheduler. Milner’s cyclic scheduler describes a scheduler for N concurrent processes. The processes are scheduled in cyclic fashion so that the first process is reactivated after the N-th process has been activated. The fairness assumptions state that a process must eventually finish its local task and then activate the next process. The property to verify is that a process must eventually be scheduled, which is true with/without the fairness assumptions. This model demonstrates the effectiveness of the partial order reduction. Without the reduction, the size of the search graph grows exponentially and thus verification soon becomes infeasible (e.g., for 15 processes).With partial order reduction, we are able to verify 400 processes reasonably fast (using less than 2 minutes). Notice that the computational overhead for handling fairness annotations are negligible, e.g., same amount of time is taken to verify the model with/without fairness. The third models the classic readers/writers problem. The readers/writers model describes a protocol for coordination of N identical readers and N identical writers accessing a shared resource. The property to verify is reachability of an erroneous situation (i.e., wrong readers/writers coordination). This mode is then annotated with fairness assumptions to state that each reader/writer must eventually finish reading/writing. This model demonstrates the effectiveness of the reduction for handling identical/similar processes.
[img[dining philosopher|experiment-por.JPG]]
The complete result can be found [[here|experiments-opt.xls]].
The complete result can be found [[here|experiments-refinement.xls]].
We conducted experiments of 5 leader election protocols for PAT version 1.2.2. The performance result can be found in [[here|fair_experiments.xls]]. The [[5 protocols|pat_models.rar]] are built inside PAT examples. Regarding the Spin model, they can be downloaded [[here|spin_models.rar]].
The experiments is conducted in a Core 2 CPU 6600 @ 2.40GHz with 2GB RAM.
We compare PAT with FDR and Spin. FDR is de facto model checker for CSP, which has been actively developing for years. We choose Spin over others because it is the most established explicit model checker and its input language is loosely based on CSP. Because there has not yet been bounded model checkers dedicated to event-based process algebras, the performance of the bounded model
checker in PAT is compared to FDR and Spin as well. PAT has been evaluated with a variety of models with two award wining SAT solvers, i.e., MiniSAT and RSAT. The experiments in this section are conducted in a 2.0 GHz Intel Core Duo CPU and 1 GB memory.
The following 4 figures summarizes the efficiency of PAT using three benchmark models, i.e., the dining philosopher problem, the classic readers/writers problem and Milner’s cyclic scheduler. The readers/writers problem describes a protocol for coordination of N readers and N writers accessing a shared resource. The property to verify is reachability of an erroneous situation (i.e., wrong readers/writers coordination). Milner’s cyclic scheduler describes a scheduler for N concurrent processes. The processes are scheduled in cyclic fashion so that the first process is reactivated after the N-th process has been activated. The property to verify is that a process must eventually be scheduled. Note that the experiment results on FDR should be taken with a grain of salt, since they run on different platforms (on the same machine) and that the results are obtained by showing a (failure) refinement relationship between the system model and a process capturing the property to verify.
For the dining philosopher example, our on-the-fly model checker (i.e., PAT-Exp) performs best to produce a counterexample. Our bounded model checker (i.e., PAT-SAT) outperforms Spin for 13 or more philosophers. One of the reasons is that the LTL to Buchi automata conversion in Spin suffers from large LTL formulae, i.e., takes more time and produces bigger automata. All verifiers outperforms FDR (except PAT-SAT for small number of philosophers because of the overhead of encoding), which is not feasible for more than 12 philosophers.
[img[dining philosopher|experiment-dp.JPG]]
For the readers/writers example, all verifiers except FDR produces a counterexample efficiently. Note that for every experiment Spin takes less than a few seconds to build model-specific executables.
[img[dining philosopher|experiment-rw.JPG]]
For the Milner’s example, the full state space (exponentially increasing) must be explored because the property to verify is true. Before using partial order reduction, PAT-Exp can only handle the size of 15, where the time goes exponentially with respect to the size. After incoperate partial order reduction, 500 milner's example can be finished in 60 seconds. The time is increased linearly, which shows how significant the optimization techniques are.The experiments on FDR and PAT-SAT produce comparable results for 12 or more processes. Given that PAT-SAT is designed to produce counterexamples efficiently, we believe its performance can be further improved by adapting the recent developments to prove true properties more efficiently. The time taken by Spin remains constant. This should probably be credited to one of the many optimization techniques that have been implemented in Spin. In the future, sophisticated optimization techniques like partial
order reduction, symmetry reduction will be incorporated into PAT.
[img[dining philosopher|experiment-ms.JPG]]
The following chart summarizes the performance our SAT-based verifier in terms of the size of the generated formula, the time needed for encoding and solving against the number of states of the model. The estimated number of states increase exponentially whereas the number of Boolean variables and the time need increase much slower.
[img[dining philosopher|experiment-sat.JPG]]
<HTML>
<HEAD>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
</HEAD>
<CENTER>
<IMG SRC="pa.JPG" BORDER="0" ALT="">
</CENTER>
</HTML>
It is generally difficult to determine which events/states are fair without the very solid understanding of the model. It can even become impossible when the model is big. Therefore, the process level fairness becomes more useful and intuitive.
For the partial order reduction, we only implemented for the weak fairness.
We introduce 3 different process level fairness: global fairness, strong fairness and weak fairness (where Spin can cover only part of weak fairness). The definitions of the 3 fairness can be found in the following paper:
M. J. Fischer and H. Jiang. Self-stabilizing leader election in networks of finite-state anonymous agents. In Proc. 10th Conference on Principles of Distributed Systems, volume 4305 of LNCS, pages 395-409. Springer, 2006.
!2009
* Yang Liu. ''[[Model Checking Concurrent and Real-time Systems: the PAT Approach|http://www.comp.nus.edu.sg/~liuyang/thesis/]]''. PhD thesis, October, 2009. (Submitted).
* Yang Liu, Jun Sun and Jin Song Dong. ''[[Scalable Multi-Core Model Checking Fairness Enhanced Systems]]''. 11th International Conference on Formal Engineering Methods (ICFEM 2009). Rio de Janeiro, Brazil, December, 2009. (Accepted).
* Jun Sun, Yang Liu, Jin Song Dong and Xian Zhang. ''[[Verifying Stateful Timed CSP using Implicit Clocks and Zone Abstraction|http://www.comp.nus.edu.sg/~sunj/Publications/ICFEM09a.pdf]]''. 11th International Conference on Formal Engineering Methods (ICFEM 2009). Rio de Janeiro, Brazil, December, 2009. (Accepted).
* Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu and Jin Song Dong. ''[[Fair Model Checking with Process Counter Abstraction|publications/fm09Counter.pdf]]''. The sixth International Symposium on Formal Methods (FM 2009). pages 123 - 139, Eindhoven, the Netherlands, November, 2009. ([[Slides|publications/fm09Counter.zip]])
* Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. ''[[Model Checking Lineariability via Refinement|publications/linearizability.pdf]]''. The sixth International Symposium on Formal Methods (FM 2009). pages 321-337, Eindhoven, the Netherlands, November, 2009. ([[Slides|publications/linearizability.ppt]])
* Jun Sun, Yang Liu, Jin Song Dong and Jun Pang. ''[[PAT: Towards Flexible Verification under Fairness|http://www.comp.nus.edu.sg/~sunj/Publications/cav09.pdf]]''. The 21th International Conference on Computer Aided Verification (CAV 2009), Grenoble, France, June, 2009. ([[Bib|http://www.comp.nus.edu.sg/~sunj/bibs.html#cav09]], [[Slides|http://www.comp.nus.edu.sg/~pat/publications/cav-slides.ppt]]).
* Jin Song Dong and Jun Sun. ''Towards Expressive Specification and Efficient Model Checking'' (invited tutorial). The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), page 9, Tian Jing, China, July, 2009. ([[Slides|publications/taseTutorial.zip]]).
* Yang Liu, Jun Pang, Jun Sun and Jianhua Zhao. ''[[Verification of Population Ring Protocols in PAT|http://www.comp.nus.edu.sg/~sunj/Publications/tase09b.pdf]]''. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pages 81 - 89, Tian Jing, China, July, 2009. ([[Slides|publications/tase09.ppt]]) //This paper presents the results of applying PAT for verifying population ring protocols. A previously unknown bug in a protocols which works under strong global fairness has been revealed.//
* Jun Sun, Yang Liu, Jin Song Dong and Chun Qing Chen. ''[[Integrating Specification and Programs for System Modeling and Verification|http://www.comp.nus.edu.sg/~sunj/Publications/tase09.pdf]]''. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pages 127 - 135, Tian Jing, China, July, 2009. ([[Slides|publications/language.zip]]). //This is a white paper on PAT's specification language (named CSP#). It contains the design philosophy of CSP# and a multi-lifts case study. //
* Shao Jie Zhang, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen and Yanhong A. Liu. ''[[Formal Verification of Scalable NonZero Indicators|http://www.comp.nus.edu.sg/~sunj/Publications/seke09.pdf]]''. The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE 2009). USA. (Accepted). //This paper presents the results of applying PAT for verifying the newly proposed Scalable NonZero Indicators algorithm.//
!2008
* Jun Sun, Yang Liu, Jin Song Dong and Hai H. Wang. ''[[Specifying and Verifying Event-based Fairness Enhanced Systems|http://www.comp.nus.edu.sg/~sunj/Publications/icfem2008.pdf]]''. The 10th International Conference on Formal Engineering Methods (ICFEM 2008). Japan. [[Bib|http://www.comp.nus.edu.sg/~sunj/bibs.html#icfem08b]]. //This is a refereed paper on how to annotate individual events in event-based compositional processes with fairness and then perform system analysis under fairness.// [[Slides|icfem08.ppt]]
* Jun Sun, Yang Liu and Jin Song Dong. ''[[Model Checking CSP Revisited: Introducing a Process Analysis Toolkit|http://www.comp.nus.edu.sg/~sunj/Publications/ISoLA08.pdf]]''. The Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008). Greece.[[Bib|http://www.comp.nus.edu.sg/~sunj/bibs.html#isola08]]. //This is a refereed paper on applying partial order reduction to CSP based system verification through refinement checking.//
* Jun Sun, Yang Liu, Jin Song Dong and Jing Sun. ''[[Bounded Model Checking of Compositional Processes|http://www.comp.nus.edu.sg/~sunj/Publications/TASE2008.pdf]]''. The 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), Nanjing, China, June 17-19, 2008. [[Bib|http://www.comp.nus.edu.sg/~sunj/bibs.html#tase08]]. //This is a refereed paper on the bounded model checker implemented in PAT. Notice that due to various reasons (mainly lack of human power), this component has been suspected indefinitely. Note that the experimental results presented in this paper on FDR can be improved significantly with a slightly different modeling.//
* Yang Liu, Jun Sun and Jin Song Dong. ''[[An Analyzer for Extended Compositional Processes|http://www.informatik.uni-trier.de/~ley/db/conf/icse/icsec2008.html#LiuSD08]]''. ICSE Companion, 2008. [[Bib|http://www.comp.nus.edu.sg/~sunj/bibs.html#icse08a]]. //This is an informal tool paper presented at 30th International Conference on Software Engineering 2008 (ICSE 2008) to demonstrate a very primitive version of PAT. //
The [[readers/writers|http://en.wikipedia.org/wiki/Readers-writers_problem]] problem describes a protocol for coordination of N readers and N writers accessing a shared resource.
The CSP definition of Readers-Writers Problem of size N is defined as follows.
<HTML>
<HEAD>
<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">
</HEAD>
<CENTER>
<IMG SRC="rw.JPG" BORDER="0" ALT="">
</CENTER>
</HTML>
The property to verify is reachability of an erroneous situation (i.e., wrong readers/writers coordination).
//[]<>error//
The following defintion is the MS example with size 2.
====================Process Definitions====================//
Reading0()=Controller;
Reading1()=((startread->Reading2)[](stopread->Reading0));
Reading2()=(stopread->Reading1);
Writing()=((stopwrite->Controller)[](stopread->(error->Writing)));
Writer0()=(startwrite->(stopwrite->Writer0));
Writer1()=(startwrite->(stopwrite->Writer1));
Reader1()=(startread->(stopread->Reader1));
Reader0()=(startread->(stopread->Reader0));
Controller()=((startread->Reading1)[]((stopread->(error->Controller))[](startwrite->Writing)));
aReadersWriters()=(Controller||(Reader0|||Reader1)||(Writer0|||Writer1));//
============================LTL Definitions============================//
LTL(AlwaysError=[]<>error);//
PAT is designed to be a self-contained framework for all kinds analysis techniques for concurrent/sequential systems. Naturally, we only explored and realized (and invented) a few of them, namely on-the-fly explicit model checking for state/event LTL, reachability analysis and refinement checking (with or with data refinement). In order to be state-of-the-art, we are actively developing PAT to cope with latest formal-automated system analysis techniques.
The following sketches some of our future plans. ''If you are interested, please [[contact|About Us]] us for research collaboration. ''
* Refinement checking for systems with fairness constraints; We are looking for both theories and algorithms. This is an extreme difficult problem (with extreme high computational complexity).
* Systematic symmetry reduction for general systems; We are looking for ways of applying symmetry reduction techniques to general systems without much changing of the modeling language. (in progress).
* Complete unit testing; We have a set of black box testing cases and we plan to apply rigorous testing techniques (e.g., SPEC#) to each and every non-trivial algorithms/classes. (in progress).
* Better (e.g., shorter) counterexample generation and display function to get the minimum counter example/strongly connected graph.
* New application domains for PAT; In particular, we are looking into domains like security protocols, distributed algorithms, etc.
* Parameterized refinement checking.
* Orc module implementation (in progress).
* Graphic User Interface for Drawing Processes (design stage).
* Refactoring Functions for the model editing: Goto Definition (for variable or process), Rename (variable and processes), (design stage).
Finished Features:
* [[25, Sep, 2009: PAT supports user defined data structures]] (Version 2.7.0).
* Time Refinement Verification (Version 2.7.0).
* Dynamic c# library importing and loading. (Version 2.6.0)
* I18N support and New Model Wizard. (Version 2.5.0).
* Real-Time System Module implementation for the verification of real time systems. (Version 2.5.0).
* System architecture improvement. (Version 2.4.0)
* Parameterized LTL Verification under fairness. (Version 2.2.0)
* Process level Fairness Implementation. (Version 2.1.0)
* Parallel verification for LTL properties (with fairness events). (Version 2.0.0)
* Improve the language Syntax and user better expression evaluation techniques. (Version 1.3.1)
* Add syntactical sugar for [], <>, <condition> to make it easy to use for non-CSP users. (Suggested by Prof Annie Liu) (Version 1.3.1)
* Implement data refinement checking functions.
* [[Accept C# code as customized functions]]
* Refinement checking optimization
* Implement better counter example display function to get the minimum counter example/strongly connected graph.
* [[Process level fairness is supported: include global, strong and weak fairness]]
* [[Add the syntax checking after parsing to rule out invalid/un-declared variables usage]]
* [[Weak Fair and Strong Fair annotations are supported by PAT now]]
* On-the-fly model checking: to verify the CSP processes with fair events. On-the-fly model checking is much faster if there is an counterexample and can avoid full state search.
* Partial Order Reduction is implemented in the PAT.
* Add the support for parameters in the Bounded Model Checking. (Global Variables are not supported)
* Reachability checking is supported.
* Refinement Checking with Partial Order Reduction. Hence, PAT can be treated as a replacement of FDR tool now.
!''PAT''
[img[PAT|PAT.JPG]]
!''Simulator''
[img[Simulator|Simulator.JPG]]
!''Buchi Automata Viewer''
[img[BAViewer|BAViewer.JPG]]
!''Model Checker''
[img[Model Checker|mc.JPG]]
The docking control is used in the simulation window with dockable "data pane" and "event and trace pane". In this way, there will be more space for graph panel.
Icons are added to the buttons to make them more meaningful.
All possible exceptions will be caught to prevent crashing of the system.
An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems
PAT: Process Analysis Toolkit
Specification editor accepts the CSP specifications and LTL properties defined in [[Specification|How to write Process Definitions]] and [[LTL|How to write LTL Formulae]] respectively.
Specification editor has an extremely user friendly user interface with following features:
*Complete text editing functions
*Syntax highlighting
*Multi-threading execution
*Multi-documents environment
!System Architecture
Starting from version 2.0, PAT is developed to be a generic framework, which can be easily extended to support new modeling languages or new assertion languages (as well as dedicated verification algorithms). The system architecture is shown in the following figure.
<HTML>
<CENTER>
<IMG SRC="./Architecture.jpg" BORDER="0" ALT="">
</CENTER>
</HTML>
In PAT, each language is encapsulated as one module with predefined APIs, which identify the (specialized) language syntax, well-formness rules as well as (operational) formal semantics, and loaded at run time according to the input model. This architecture allows new languages to be developed easily by providing the syntax rules and semantics. Two modules have been developed currently, namely Communicating Sequential Processes (CSP) module, Real-Time System (RTS) Module and Web Service (WS) module. An extensible library of assertions, together with their verification algorithms, have been designed to operate on the underlying shared semantic models of the modules and therefore easily applicable to all modules. For instance, the automata-based LTL model checking algorithm, with partial order reduction, is applied to both modules.
!System Components
The following are the four main components of PAT.
* Editor: User friendly editing envinronment (with advanced syntax editing features) for introducing models.
* Parser: Smart parsing to apply process equivalence laws to simply system models as well as associating assertions with the dedicated checker.
* Simulator: User friendly simulator for interactively and visually simulating system behaviors; by either random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
* Model Checkers: Click button model checker for deadlock-freeness verification, reachability analysis, state/event linear temporal logic verification (with or with fairness) and refinement checking (with or without checking data components).
<HTML>
<CENTER>
<IMG SRC="./flow-2MC.png" BORDER="0" ALT="">
</CENTER>
</HTML>
The above highlights the work flow of PAT. The parser takes in the system model and then builds the internal representation. Different assertions are associated with the dedicated analyzers respectively. If the assertion involves LTL, it is automatically translated into an equivalent Buchi automaton. The internal representaion of the model can be fed to the simulator for simulation or the verifiers for verification. If a counterexample is generated, the counterexample may be fed to the simulator.
!Software Components
PAT is implemented using C# 2.0 and Visual Studio 2008. The following external components are used or embedded in the PAT package.
* PAT's parser is based on [[Antlr Parser Generator|http://www.antlr.org/]].
* The LTL to Buchi Automata Converter in PAT is based on [[Paul Gastin's work|http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php]] on fast translation from LTL to Buchi automata. We have translated the original c++ code to C#.
* PAT's simulator is based on [[Graph Layout Execution Engine (GLEE)|http://research.microsoft.com/users/levnach/GLEEWebPage.htm]] from Microsoft. Recently, GLEE is commerialized and renamed to [[MSAGL: Microsoft Automatic Graph Layout|http://research.microsoft.com/en-us/projects/msagl/]].
* PAT's editor (i.e., mulit-document environment) is based on [[dotnetfireball|http://www.codeplex.com/dotnetfireball]].
* PAT's unit testing component is done using [[NUnit|www.nunit.org]].
!Screen Shots
Screen Shots of PAT version 2.2.0 is avaiable [[HERE|Screen Shots]].
!User Manual
The user manual is available ''[[online|OnlineHelp/index.htm]]''.
The CHM version can be downloaded ''[[HERE|OnlineHelp/Help.zip]]''.
If you are interested in the technical details of PAT, refer to our [[Publications]].
!Documantation and Tutorials of PAT
1 [[PAT Getting Started|pat_getting_startted.ppt]] (Power Point). A starting guild of how to use PAT. Some simple syntax examples are [[here|example.zip]].
2 [[CSP Slides|csp-slide.pdf]] (PDF). CSP introduction lecture notes.
3 [[CSP Semantics 1|csp1.pdf]], [[CSP Semantics 1|csp1.pdf]] (PDF). CSP Semantics Introduction lecture notes.
4 [[PAT Presentation|pat.ppt]] (Power Point). Slides for PAT Talks, including fairness definitions and refinement checking.
5 [[Model Checking|model_checking.pptx]]. Slides for a general introduction to Model Checking.
6 [[PAT Advanced Topics|pat_talk_2.ppt]] (Power Point). The peterson's algorithm can be download [[here|ps2.csp]]
7 [[PAT Presentation Slides on ICFEM 08|icfem08.ppt]] (Power Point).
8 [[PAT Presentation Slides on CAV 09 about fairness|publications/cav-slides.ppt]].
9 [[PAT Input Language CSP# Slides on TASE 09|publications/language.zip]] (Power Point).
10 [[Verify Population Protocol Slides on TASE 09|publications/tase09.ppt]] (Power Point).
11 [[Towards Expressive Specification and Efficient Model Checking Slides on TASE 09|publications/taseTutorial.zip]] (Power Point).
12 [[Model Checking Lineariability via Refinement Slides on FM 09|publications/linearizability.ppt]] (Power Point).
13 [[Fair Model Checking of Parameterized Systems Slides on FM 09|publications/fm09Counter.zip]] (Power Point).
!''Version 2.7.0 Build 11273''
13, Nov, 2009
1 Bug fixing for the self choice composition in parsers.
2 Bug fixing for parallel alphabet calculation of recursive processes.
3 Bug fix for LTL like !(<>P || <>!P).
4 OutOfMemory exception is caught properly and PAT will not crash for it.
!''Version 2.7.0 Build 11141''
24, Oct, 2009
1 [[24, Oct, 2009: Warning List is supported. PAT makes the modeling easier!]]
!''Version 2.7.0 Build 11121''
23, Oct, 2009
1 Process Counter Variable is supported in event prefix
2 Bug fixing for using atomic with parallel operator
3 Exceptions are caught for config files missing or no-writting access rights.
4 Bug fixing for using local variables
!''Version 2.7.0 Build 11055''
09, Oct, 2009
1 Japaness Language is updated
2 Bug fixing.
!''Version 2.7.0 Build 10964''
25, Sep, 2009
1 Bugs are fixed for RTS module.
2 C# library supporting is improved. [[25, Sep, 2009: PAT supports user defined data structures]]
3 Performance improvement for all modules by changing the expression evaluation.
4 Examples for alternating bit protocols are added.
!''Version 2.7.0 Build 10711''
15, Sep, 2009
1 Bugs are fixed for RTS module.
2 PaceMaker example is completed for 16 modes.
3 Performance improvement for all modules. We implemented a Hashtable by ourself to replace the .NET built-in Dictionary class.
4 ifa and guard constructs are disabled in RTS module for the confusing semantics.
!''Version 2.7.0 Build 10511''
08, Sep, 2009
[[05, Sep, 2009: PAT 2.7.0 is released!]]
1 (Timed) Divergence-free assertion is supported.
2 Bugs fixing in the RTS module.
!''Version 2.7.0 Build 10427''
05, Sep, 2009
[[05, Sep, 2009: PAT 2.7.0 is released!]]
!''Version 2.6.0 Build 10063''
10, July, 2009
1 parser supports multi-dimentional array initialization for all the three modules.
2 change Submit model to Email model to allow user to send model to others quickly.
3 Two new puzzle examples are added.
4 user manual update for new parser and user feedback.
!''Version 2.6.0 Build 10016''
24, June, 2009
1 Several bug fixing in RTS module.
2 Implemented the latex generation function for RTS, and fixed some bugs in CSP latex generation functions
!''Version 2.6.0 Build 9922''
15, June, 2009
1 Bug in parsers are fixed for Constants used as Integer directly
2 X operator is not allowed in RTS module
3 User Manual is updated to the latest version 2.6.
!''Version 2.6.0 Build 9909''
12, June, 2009
[[09, Jun, 2009: PAT 2.6.0 is released!]]
!''Version 2.6.0 Build 9847''
9, June, 2009
[[09, Jun, 2009: PAT 2.6.0 is released!]]
!''Version 2.5.0 Build 9622''
4, June, 2009
1 Bugs in the Real-Time System Module are fixed.
2 within syntax is supported in Real-Time System Module. e.g., P within[4]/ P within[3,10]. User Manual is to be updated.
3 Railway control example is added in for RTS module.
!''Version 2.5.0 Build 9580''
3, June, 2009
1 Bugs in the Real-Time Module are fixed.
2 Event level fairness checking are considering tau and termination events now.
!''Version 2.5.0 Build 9544''
2, June, 2009
[[02, Jun, 2009: PAT 2.5.0 is released!]]
!''Version 2.4.0 Build 8808''
7, May, 2009
1 The Needham-Schroeder Public Key Protocol example is added.
2 Process parameters can be used in channel input for both CSP and WS module
3 Model Checking forms are made consistent
4 Bugs of parallel verification are fixed.
5 UI bugs fixed
6 User Manual is updated to the latest syntax
!''Version 2.4.0 Build 8710''
30, April, 2009
[[30, Apr, 2009: PAT 2.4.0 is released!]]
!''Version 2.3.0 Build 8000''
13, April, 2009
[[13, Apr, 2009: PAT 2.3.0 is released!]]
!''Version 2.2.0 Build 7862''
8, April, 2009
1 Rubik's Cube example is added.
2 Cut number popup is added in the simulator for infinite processes.
3 Updated Parameterized Leader Election to make it smaller.
4 Constants are allowed in the process invocation
5 parser checking for array index is added: must be an integer value or expression.
6 enum is supported. see user manual.
7 Latex buttons and icons are added (beta version)
8 Parallel model checking bug fixed.
9 Fairness check for concrete counterexample is added.
!''Version 2.2.0 Build 7760''
2, April, 2009
1 External Choice will not distinguish tau event and normal event. Although this is different from the original CSP semantics, but for the simplicity of the modeling, we adopt this new semantics.
2 Boolean variables can be directly used in the condition of if/while/conditional choice.
3 Bugs in simulator are fixed.
!''Version 2.2.0 Build 7715''
1, April, 2009
1 PAT2 Shortcut links are fixed. especially for vista user to get rid of UAC.
2 Simulate Counter Example Button is renamed to Simulate Witness Trace
3 Add UNKNOWN result to LTL assertion and reachability assertion
!''Version 2.2.0 Build 7688''
30, March, 2009
1 What's new link is added to the GUI and update screen
2 Invisible Events: User can explicitly write invisible event (i.e., τ event) by using keyword tau, e.g., tau -> Stop. In the tau event, statement block can still be attached. With the support of tau event, you can avoid using hiding operator to explicitly hide some visible events by name them tau events. The second way to write an invisible event is to skip the event name of a statement block, e.g., {x=x+1;} -> Stop, which is equivalent to tau{x=x+1;} -> Stop.
3 out of memory exception is handled properly
4 Refinement checking for hiding expression's bug is fixed
5 Simulator window edge tooltip is simplified.
6 Parser for channel input is implemented: no parameter or global variables are allowed in channel input.
7 Added support for parsing "P = ||| x :{1..2} ( a -> Skip \ {a.x});"
8 User Manual is updated to latest version.
!''Version 2.2.0 Build 7621''
27, March, 2009
[[27, Mar, 2009: PAT 2.2.0 is released!]]
!''Version 2.1.0 Build 7082''
9, March, 2009
[[09, Mar, 2009: PAT 2.1.0 is released!]]
!''Version 2.0.0 Build 6360''
21, Jan, 2009
1 New examples are added for stablizing leader election protocols
2 Saving Button bugs are fixed.
3 Option form is improved.
4 Allow auto saving when buttons are clicked.
5 Bug fixing for WS module.
!''Version 2.0.0 Build 6091''
9, Jan, 2009
1 Each document tab can be closed/saved by using right mouse click on the tab.
2 UI update to fix some bugs and improve the usability
3 Web Service Module is implemented. Currently, we have finished all functions: verification, simulation, synthesis
But this module still needs more testing.
4 Example updates for lift system, keyless car system and pace maker examples.
!''Version 2.0.0 Build 5595''
5, Jan, 2009
1 Icons added for the CSP and WS files
2 Exception Dialog is added
3 Choregraphy Synthesis in WS module is implemented.
4 Archectecture improvement.
5 Road Assistance Example for WS is added.
!''Version 1.3.1 Build 5530''
28, Dec, 2008
Strong Global Fair algorithm is improved. The performance is improved significantly if the found SCCs are big.
!''Version 1.3.1 Build 5515''
21, Dec, 2008
1 [[21, Dec, 2008: PAT 1.3.1 is released!]]
2 [[Launch PAT after installation option is added.]]
3 Manual is updated to version 1.3.1.
!''Version 1.3.0 Build 5478''
17, Dec, 2008
1 Manual is updated for the typos in tutorial and language reference. The completed grammar rules are added.
2 Parser supports channel events like "c!1", "c?3". ! and ? are special charactors, it is not possible to put them into LTL assertions like normal events eat.0
So we decided to user quotation mark to group them as single event. Hope this is acceptable solution.
3 Upon the request, we changed the parser so that the semi colon of the last expression in event statement block is optional.
e.g., "event{a = a +1} -> Stop" is valid syntax. This will make the modelling easier.
!''Version 2.0.0 beta''
10, Dec, 2008
The Web Service Module is integrated in PAT.
!''Version 1.3.0 Build 5450''
04, Dec, 2008
New Manual is updated.
Parser bug fixed.
Keyless Car System Example is added.
!''Version 1.3.0 Build 5423''
26, Nov, 2008
[[Display of the current enabled events is fixed.]]
Unhandled exceptions of PAT is displayed with better details.
Parser typo fixed.
!''Version 1.3.0 Build 5395''
25, Nov, 2008
[[25, Nov, 2008: PAT 1.3.0 is released!]]
!''Version 1.2.9 Build 5202''
21, Nov, 2008
init event is added to the system.
UI improvement.
!''Version 1.2.9 Build 5152''
19, Nov, 2008
[[19, Nov, 2008: PAT 1.2.9 is released! Please re-install PAT!]]
!''Version 1.2.8 Build 4917''
15, Nov, 2008
[[15, Nov, 2008: PAT 1.2.8 is released!]]
!''Version 1.2.7 Build 4917''
11, Nov, 2008
Bug fixed for negative operator.
Parser is improved
csp can be opened by PAT directly now.
!''Version 1.2.7 Build 4850''
06, Nov, 2008
Bug fixed for the exmaple loading.
!''Version 1.2.7 Build 4848''
05, Nov, 2008
Bugs in the limited depth search is fixed.
Partial Order Reduction is disabled for the limited depth search.
!''Version 1.2.7 Build 4824''
04, Nov, 2008
[[04, Nov, 2008: PAT 1.2.7 is released!]]
!''Version 1.2.6 Build 4709''
17, Oct, 2008
1 Bugs in generating counter example is fixed.
2 Add multi-threading for the counter example generating prcoess
3 Parser supports variables in alphabets declarations, also, if the variable is not declared in the process definition, the error message will popup.
!''Version 1.2.6 Build 4680''
16, Oct, 2008
Some bug fixing and performance improvement.
!''Version 1.2.6 Build 4600''
13, Oct, 2008
Conditional Choice <<>> is removed from the syntax.
sdefine and sequal is added
Bug fixing for FD verification
Refinement checking speed improvement.
GUI improvement.
!''Version 1.2.6 Build 4531''
10, Oct, 2008
Bug fix for the Event Prefix class.
The sequence class is optimized using algebra law. Got a big performance improvement.
Linearizability examples are added back.
!''Version 1.2.6 Build 4401''
[[06, Oct, 2008: PAT 1.2.6 is released!]]
!''Version 1.2.5 Build 4268''
[[03, Oct, 2008: PAT 1.2.5 is released!]]
!''Version 1.2.4 Build 3140''
11, Sep, 2008
The structure is improved.
Bugs in the counter example display are fixed.
!''Version 1.2.3 Build 2684''
8, Aug, 2008
[[Accept C# code as customized functions]]
Mailbox problem is built-in.
!''Version 1.2.2 Build 2566''
6, Aug, 2008
Bugs in the LTL model checking is fixed.
User Manual is updated
!''Version 1.2.2 Build 2512''
5, Aug, 2008
Bugs in the LTL model checking is fixed.
Peterson Algorithm is added into the system.
!''Version 1.2.2 Build 2492''
31, July, 2008
MSAGL is integrated into PAT.
Progress bar in the model checking is removed
Bugs in LTL2BA conversion are fixed.
Simulation Direction choice is added: Top-Down or Left-Right.
Auto-update function is added to pat.
!''Version 1.2.1 Build 2301''
23, July, 2008
Performance (both time and memory) for the refinement checking is improved.
Timer is added in the model checking UI.
One Linearizibility example is added in.
!''Version 1.2.1 Build 2213''
22, July, 2008
Linearizibility examples are added in.
One more leader elction protocol is added in.
two puzzle examples are added in.
Bug in refinement check is fix.
The local variable is considered in the partial order reduction of refinement checking.
Syntax color for Skip and Stop is changed to Navy.
!''Version 1.2.1 Build 1988''
16, July, 2008
Simulator's User interface is improved:
1 Current enabled events are highlighted in blue
2 hidden events are shown as [event].
Two leader election protocol is added as built-in examples.
!''Version 1.2.1 Build 1952''
14, July, 2008
The couter example information is totally redesigned for better speed and code structures.
Counter example generation and simulation's bugs are fixed.
!''Version 1.2.0 Build 1812''
10, July, 2008
[[Process level fairness is supported: include global, strong and weak fairness]]
Leader Election protocol examples are implemented and built-in PAT.
Counter example simulation is improved.
Strongly connected components simulation is improved.
Counter exampple generation bugs fixed.
!''Version 1.1.5 Build 1566''
1, July, 2008
Fairness loop detection bug fixed and performance improved.
Verification details added: Search Depth, States visited, Transitions.
Unary Operator bug fixed.
The process level fairness coding started.
!''Version 1.1.5 Build 1506''
7, June, 2008
Built-in examples are corrected.
Console is updated to latest model checker.
!''Version 1.1.5 Build 1484''
2, June, 2008
Temporal operators are supported in PAT:
G (always)
F (Eventually)
U (until)
V | R (realease)
X (next)
The example creation form is improved to add more explainations.
The error message of wrong LTL properties is improved.
!''Version 1.1.5 Build 1374''
25, May, 2008
Parallel/interleave Parsing Errors are fixed.
Repeated properties can be detacted and reported.
Specification Description panel is added.
The embedded example are completely re-written now, a new example BridgeCrossing Exmaple is added.
GetAlphabet Method and ClearConstant Method. The alphabet of a process is default to be the events constituting the process (all parameter instantiated) expression.
Support constant in declarations definition (and possible elsewhere).
Report error message if an array declaration contains a negative number.
Verification user interface is improved and more meaningful icons are used.
!''Version 1.1.5 Build 1137''
7, May, 2008
The simulation window' docking display is improved.
The graph states info in the simulation window is added.
!''Version 1.1.5 Build 1128''
5, May, 2008
Build Number is added into the system for better tracking. The build number is auto-increased.
Parser is redesigned using two time AST parsing.
[[Add the syntax checking after parsing to rule out invalid/un-declared variables usage]]
[[Weak Fair and Strong Fair annotations are supported by PAT now]]
In the main UI, Output panel display bug is fixed.
StateGuard class is replaced by using IfProcess class.
Unit Testing via [[NUnit|www.nunit.org]] is added, hope later we can add more test cases into the system.
[[Simulation window is redesigned completely]]
!''Version 1.1.5 revision 1''
25, April, 2008
User interface of simulation form is improved to allow user adjust the width of the different columsn.
The loops in the counter example is highlighted, and highlighted in simulator.
If process is implemented for the easy handling of multiple external choice operator.
Bug fixing of Bounded Model Checking: the TLS tree tranversal method is wrong.
Bug fixing in if expression evaluation: the else clause null checking is missing in build var method.
Strong fair and weak fair annotations are added in the system, the corresponding model checking algorithms are updated.
!''Version 1.1.5''
25, April, 2008
User interface of model checking form is improved.
The loops in the counter example is highlighted in the output box, and also highlighted in simulator.
If process is implemented for the easy handling of multiple external choice operator.
Bug fixing of Bounded Model Checking: the TLS tree tranversal method is wrong.
Bug fixing in if expression evaluation: the else clause null checking is missing in build var method.
Strong fair and weak fair annotations are added in the system, the corresponding model checking algorithms are updated.
!''Version 1.1.4 revision 1''
23, April, 2008
Allow Constant in the index parallel and interleave processes
Exception handling is added in the Simulation and Model Checking interface so that the application will not crash due to the invalid model.
Various Bug fixing
!''Version 1.1.4''
31, March, 2008
Refinement checking is implemented.
Installation file is created.
Batch Mode Console interface is created for PAT.
!''Version 1.1.3''
20, Feb, 2008
Partial Order reduction is added to bounded model checking.
channel is supported
bug fixed in simulator and model checkers.
Syntax sugar for the Interleave and Parallel Construct is added.
!''Version 1.1.2''
16, Jan, 2008
Libra is renamed to PAT (Process Analysis Toolkit) to avoid the conflict with Microsoft Libra searching system.
Reachbility checking is supported.
Assertions is introduced for various model checking and refinement checking.
Combine the Model Checking and Bounded Model Checking in one Window.
Performance optimizations and bug fixing.
The support of array is added.
Fair events are added to the examples.
!''Version 1.1.1''
09, Jan, 2008
Bug fixed for the model checking algorithms.
Partial Order Reduction option is added in the user interface
SAT model checking can handle Local Parameters.
!''Version 1.1''
03, Jan, 2008
Partial Order Reduction is added, which gives a great performance improvement for some cases.
On-the-fly model checking algorithms are implemented for the specifications with or without fairness. We implemented the improved iterative Tarjan algorithms.
Counter example simulation is added in the model checking windows.
System simulation is improved and simplified.
!''Version 1.0''
28, Nov, 2007
Global variables and functions are introduced into Libra.
Dike is renamed to Libra due to its pronunciation.
More testing are needed.
!''Version 0.9''
10, Nov, 2007
Model Checker based on SAT solvers are added into the system.
System is restructured for extensible design and standard naming convention.
!''Version 0.8''
15, Oct, 2007
Simulator is added into the system.
!''Version 0.7''
02, Oct, 2007
Parser is re-implemented to support all possible definitions specifications.
Verification can be done for user selected Process definitions.
LTL error message reporting function added.
Syntax highlighting is added.
!''Version 0.6''
26, Sep, 2007
More meaning parsing error report for the specification is added.
Full set of editing functions are added.
The tool is named Dike officially.
LTL parser crashing is solved.
!''Version 0.5''
10, Sep, 2007
Comprehensive Multi-tab editing environments are integrated into the Dike.
The implementation is based on FireBall.
LTL parsing options are added.
Peterson's Algorithm Examples are added.
!''Version 0.4''
23, August, 2007
The Buchi Automata Viewer is integrated.
MC algorithms improved: Finite processes can be checked under fairness conditions
!''Version 0.3''
10, August, 2007
The LTL to BA convector is added.
Dinning Philosophers Examples are added.
!''Version 0.2''
2, August, 2007
The parser of CSP is added, which is based on Antlr 3.0.
Get All traces function is added.
Several bug fixing for the model checking algorithms
The previous closure algorithm is improved for fast feasible and model checking.
!''Version 0.1''
25, July, 2007
The first implementation of the UI is finished.
Feasibility and Model checking algorithms is completed.
Originally, PAT supports only weak live and strong live events. To make PAT more useful, weak fair and strong fair events are supported.