Welcome to TiddlyWiki created by Jeremy Ruston, Copyright © 2007 UnaMesa Association
!''What's new in PAT 2.8.0''
In this release, the main achievement is that safety properties detection and verification is implemented in PAT (in all modules). Furthermore, modeling languages in CSP and RTS modules are improved for better expressiveness power and parsing precision. Other updates include new examples and bug fixing.
''Safety property detection''
Safety properties verification is relatively easy and fast. However, sometimes it is hard to tell whether a LTL property is a safety one or liveness one. In this release of PAT, we implement the safety property detection algorithm to distinguish them from liveness ones. For all safety properties, we implemented a simple DFS model checking algorithm to speedup the verification. All these are automatic.
''Assertion process is supported in all modules''
Assertion process allows user to add an assertion in the program and PAT simulator and verifiers will check the assertion at run time. If the assersion is failed, a PAT runtime exception will be thrown to the user and the eveluation is stoped. The syntax of Assertion is as follows,
//var x = 1;//
//P = assert(x > 0); e{x = x-1;} -> P;//
''Parsing warning is added for if/while expression inside event assignment with no body''
''LTL to Buchi Automata Converter is added into the UI''
We provide a simple ultility under toolbar "Tools" to allow user to generate a BA from LTL directly.
''Others''
1 User manual is updated to latest implementation.
2 Ctrl + W is supported to close the current tab.
3 UI exceptions are captured3 Fix the bugs in parsing, GUI and other places.
!''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.
All experiments with configuration information, dataset are in the process of being standardized and made available at PAT website. The data is to show that PAT’s model checking library is highly optimized.
Details about the experiments can be found in [[Experiments]].
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
After some efforts, we glad to release PAT 3.1.0, which can run in all platforms: Linux, Mac OS and more!
The solution is to use [[Mono|http://www.mono-project.com/Main_Page]], which is an open source, cross-platform, implementation of C# and the CLR that is binary compatible with Microsoft.NET.
Install PAT 3.x in Linux, Unix, Mac OS or more, please follow these steps:
*You should install mono tool in your system which is freely available. Please download from [[here||http://www.go-mono.com/mono-downloads/download.html]] according to your OS.
*Download PAT 3.x. But choose the ''directly executable version'' to some place in your computer.
*In your computer, start terminal application, using the command cd to the directory where you put ''"PAT 3.exe"'';
*Type the command ''mono "PAT 3.exe"'' into terminal. Bingo! You will see the GUI of our PAT.
Note that running PAT in Mono, the performance can be (much) slower than runing PAT in Windows.
Here is some prelimenary experiment on the CSP linearizability Stack example, with same laptop but different OS.
<html>
<TABLE>
<TR><TD>
<TD><B>Mac OS</B>
<TD><B>Windows</B>
<TR><TD>stack length: 8
<TD>75.39s
<TD>24.69s
<TR><TD>stack length: 9
<TD>86.42s
<TD>30.74s
<TR><TD>stack length: 10
<TD>111.04s
<TD>39.55s
</TABLE>
</html>
There are some known bugs when running PAT in Mono:
1) Email sending in Mac OS is not working. This is an issue of Mono library.
2) Sometimes the first line of the model (or part of the model) is invisible, and user should click there to see the text.
3) in simulation window, it works very well except the Save and Export buttons. These two buttons are invisible before you click them.
If you find bugs and issues when running PAT in Mono, please do [[contact us|About Us]].
Other update in the version 3.1.0 including bug fixing and new examples.
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
!Experiments for FM 2011 Submissions
[[Paper 16: Developing a Model Checker for Probabilistic Real-time Hierarchical Systems|http://www.comp.nus.edu.sg/~pat/fm/prts/]]
[[Paper 23: Compositional Partial Order Reduction for Concurrent Systems|http://www.comp.nus.edu.sg/~pat/fm/cpor]]
[[Paper 40: Building Model Checkers Made Easy|http://www.comp.nus.edu.sg/~pat/fm/system]]
[[Paper 58: Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare|http://www.comp.nus.edu.sg/~pat/fm/ai/]]
[[Paper 61: Automated Verifying Anonymity and Privacy Properties of Security Protocols|http://www.comp.nus.edu.sg/~pat/fm/security]]
[[Paper 101: On Combining State Space Reductions with Global Fairness Assumptions|http://www.comp.nus.edu.sg/~pat/fm/sym]]
[[Paper 68: PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers|http://www.comp.nus.edu.sg/~pat/fse/system]]
[[Paper 84: Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare|http://www.comp.nus.edu.sg/~pat/ai/]]
Find them at [[User Manual]].
!API for PAT.Common.dll
The CHM version can be downloaded ''[[HERE|OnlineHelp/API.zip]]''.
This file include all methods and fields for PAT.Common project. All module needs to follow these APIs in order to be recongnized by PAT framework.
Please refer to user manual on how to use the APIs to develop custimized module in PAT.
After some testing, PAT 3.0 is arrived. Compared with the beta version, we mainly do the bug fixing.
New features in the RTS module:
''Urgent Event''
In RTS module, we assume all the event prefix, data operation and channel communication (channel input/channel output) takes arbitrary amount of time. Sometimes, we want the events takes no time (instantaneous events). The normal approach is to use (Process within[0]) to model this requirement. In RTS module, we introduce the concept of Urgent Event to simplify this kind of modeling. The supported syntax is shown in the following examples.
event{program} ->> Process
c!x ->> Process
c?x ->> Process
Note: tau event in RTS module is an urgent event by default. A natural consequence is that, all events after hiding become tau event and take no time.
''Timed Zenoness Checking''
Because RTS module supports process constructs like deadline, it suffers from zeno executions, i.e., infinitely many steps taking within finite time. Zeno executions are unrealistic and therefore must be ruled out in model checking. It is known that zone graphs are not fine enough to distinguish zeno executions. We show that the zone graph produced by dynamic zone abstraction can be modified so that the properties are verified with the assumption of non-Zenoness.
To remove zeno executions, PAT implements Zeno checking for LTL/Deadlock assertions. Users only need to tick the "Apply Zeno Check" in the model checking form. More Zeno checking will be implemented for RTS module.
1 A set of new refinement algorithms are implemented for CSP module and PCSP module (based on anti-chain technique). For CSP module, the performance improvement is substantial for some cases.
Hence we make the new verification algorithm as default engine for refinement checking.
2 Bug fixing for RTS module (Thanks Oguzcan Oguz for reporting a number of critical errors in RTS module)
3 Bug fixing and performance improvement for BDD support for CSP and RTS modules.
4 Bug fixing in CSP module code generation function.
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!
15, Nov, 2011
1 BDD support for CSP module is ready for testing. Wild Variable is also supported.
2 RTS module supports guard and ifa now. Parsing will fail if timed process is immediately following the guard and ifa.
e.g., P = [cond](Wait[5]);
3 A number of bug fixing for parsers in all modules.
4 Skip checking inside sequential composition is added and improved for all modules.
5 using direct array in process arguments and call arguments are supported.
e.g.
var <IntArrayList> intList;
intList.Add([1, 2, 3, 4, 5]);
6 font fixing for 64bit Windows machine.
We would like to thank PAT Japanese User Group for supporting the PAT development (by providing Japanese translation and valuable feedback), promoting PAT tool and hosting us in Japan. We have special thank to Kenji Taguchi, Hiroshi Fujimoto, Masaru Nagaku, Toshiyuki Fujikura. We wish to extend the collaboration and achieve more fruitful results.
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).
!''What's new in PAT 2.9.1''
In this minor release, we introduced two new assertion: nonterminating and deterministic. Also a lot of bugs in CPS, RTS and PCSP modules are fixed. The most significant change is the Graph difference comparison function of any two simulation graph, which is a joined work with Dr Xing ZhenChang.
''Deterministic''
Given P() as a process, the following assertion asks whether P() is deterministic or not.
//#assert P() deterministic;//
Where both assert and deterministic are reserved keywords. Given a process, if it is deterministic, then for any state, there is no two out-going transitions leading to different states but with same events. E.g, the following process is not deterministic.
//P = a -> Stop [] a -> Skip;//
''Nonterminating''
Given P() as a process, the following assertion asks whether P() is nonterminating or not.
//#assert P() nonterminating;//
Where both assert and nonterminating are reserved keywords. PAT's model checker performs Depth-First-Search or Breath-First-Search algorithm to repeatedly explore unvisited states until a terminating state (i.e., a state with no further move, including successfully terminated state) is found or all states have been visited. The following process is deadlockfree, but not nonterminating.
//P = a -> Skip;//
''Graph Difference Comparison''
To compare the diffference between any two simulation graph can give user the feedback for the difference of the specifications.
In this version, we have implemented the first version of graph comparison of any two opened simulators. After the comparison, the differernce are highlighted in different colors.
This release mainly introduce more language syntax sugers, latest Antlr Parser library, GUI improvement and bug fixing.
''Language changes'':
1 The indexed booleans expressions are supported in CSP Module.
The indexed expression is a syntax sugar for grouping a list of OR or AND expressions together overal a range of variables. The syntax is following:
A typical example is as follows:
var x[3];
P = if(&& i:{0..2}@(x[i] == 0)){bingo -> Skip};
2 Index events are supported in CSP Module.
The syntax sugar indexed event list can be used in the definition of alphabets. For example:
//#define N 2;
P = e.0.0 -> e.0.1 -> e.0.2 -> turns -> e.1.0 -> e.1.1 -> e.1.2 -> e.2.0 -> e.2.1 -> e.2.2 -> P;
#alphabet P { x:{0..N}; y:{0..N} @ e.x.y }; //
The above definitions define the alphabet of process P as the set of all events except event turns appearing in its proces definition.
The syntax sugar indexed event list can be used for defining a set of events with the same prefix. For example, the definition for process dashPhil() can be rewritten as the following.
//dashPhil() = Phil() \ { x:{1..2} @ getfork.x, y:{1..2} @ putfork.y};//
3 Warning is added for non-synchronization of events and data operations.
This is a common problem raised by many users that, for the following program, can the two processes P() and Q() synchronise on the event a? If not, then how to make them synchronise on 'a' and preserve the execution of statement block ({x++}) in an atomic fashion?
//var x=0;
P() = a{x++} -> b -> P();
Q() = a -> c -> P();
System() = P() || Q();//
Answer:
''No-Synchronization on Data Operations'' is a design decision to void data race. If two data operations can synchronize, the update of the same global variable can lead to data race. Therefore, PAT will give a warning that if there one data operation and an event with same in different processes running in parallel.
Back to the question, a intuitive solution is to put the event 'a' and increment statement in an atomic action as follows:
//P() = atomic{a -> update{x++} -> Skip};b -> Skip;
Q() = a -> c -> Skip;
aSystem() = P() || Q();//
Then x will be updated right after a is engaged, and a will be synchronised.
The other possible solution could be:
//P() = a -> update{x++} -> a1 -> b -> P();
Q() = a -> a1 -> c -> P();//
4 Parsers are updated to the latest version of Antlr C# library.
''GUI''
1 Splash screen is added
2 Multi asseertion selection in the Model Checking
3 More high-lighting in the model checking output form
4 Bug fixing in the GUI
''Examples''
1 More examples are added in the LTS module.
2 Simulation Image is added to Kight Tour example in CSP Module
''Bug Fixing''
1 Bugs in external choices are fixed in all modules
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.
PAT 3.2.0 is a beta version, which includes a lot of new modules: Labeled Transition Systems Module, Timed Automata Module, Orc Module, Security Module, NesC Module, MDL Module.
This version is a preview version and will not be avaiable from auto-update.
We will keep on updating this beta version to fix the bugs and complete the user manual.
Note that ''PAT 3.2.0 is restricted to academic use only.''. If you want to use it for commertial purpose, please contact us.
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.
In this minor release, the update include the following:
1 Bugs for simulator are fixed
2 Find Usage for variables, processes, channels and declarations are supported in all modules
3 Module Generator is implemented.
4 LTS module is re-implemented.
a) The language support full syntax of CSP, except terminal process call can only drawn Process. For example, the following syntax is not valid
P = a -> Skip;
Q = b -> P;
b) a new syntax is supported in LTS under the BDD module checking
var x = *; //a process with arbitrary value
!''What's new in PAT 3.0.0''
In this version, we have done a complete system redesign for better extensibility.
PAT's UI is complete re-implemented with new text editor with improved syntax highlighting and input intellesense.
The performance of almost all assertions is improved compared with old version.
Beta version of PRTS Module is released. This module combines Probability and Real-Time for modeling Real-time probabilistic systems.
''Important Note'': PAT 3.0.0 is upgrated to .NET framework 3.5. To run PAT, you need to install .NET framework 3.5, which can be downloaded [[here|http://www.microsoft.com/downloads/details.aspx?FamilyId=AB99342F-5D1A-413D-8319-81DA479AB0D7&displaylang=en]].
Two Postdoc Research Fellow Positions on Model Checking
National University of Singapore
Highly motivated applicants are being sought to work on developing model checking techniques. The postdocs will work with the software engineering and formal methods group at National University of Singapore on further developing the PAT toolkit (http://pat.comp.nus.edu.sg).
PAT is a powerful self-contained system for modeling, simulating, and verification. It has an extensible architecture so that new modeling language, abstract techniques, and model checking techniques can be easily supported. Six modules supporting different domains have been develoed, covering concurrent, real-time, probabilistic, hierachical systems. It offers a library of model checking algorithms for a variety of properties, e.g., reachability analysis, temporal logic verification, refinement checking, verification with fairness, zone abstraction, probabilistic model checking, etc. PAT has been applied to many case studies and successfully found previously unknown bugs. It has been adopted for research and teaching in multiple universities. More details about PAT can be found at http://pat.comp.nus.edu.sg.
The applicant shall conduct research on optimizing PAT. Candidate techniques include distributed/parallel model checking, automated abstraction techniques (possibly domain specific), generalized symmetry reduction, etc. The applicant will study the PAT framework, identify the suitable state reduction techniques, design/implement the techniques in PAT. The position involves conducting basic research, developing tools, working as part of a research team, traveling, and giving presentations. The working lanugage is English.
Candidate profile:
- A PhD in Computer Science or related areas is required.
- Expertise in Formal Methods and Model Checking technology.
- Strong background in logic and discrete math.
- Strong programming skills (the language we are working with is C#).
- An established research record.
The term is currently 2 years starting immediately and can be extended.
The salary range is around 60K-85K SGD pa (1 SGD = ~ 0.75 USD).
Interested applicants should send their CV to Dr. Jin-Song Dong at dongjs@comp.nus.edu.sg.
Highly motivated applicants are being sought to work on developing model checking techniques. The postdocs will work with the software engineering and formal methods group at National University of Singapore on further developing the PAT toolkit (http://www.patroot.com).
PAT is a powerful self-contained framework for modeling, simulating, and verification. It has an extensible architecture so that new modeling language, abstraction techniques, and model checking techniques can be easily supported. Currently, 11 modules supporting different domains have been developed, covering concurrent, real-time, probabilistic, hierarchical systems. It offers a library of model checking algorithms for a variety of properties, e.g., reachability analysis, temporal logic verification, refinement checking, verification with fairness, zone abstraction, probabilistic model checking, etc. PAT has been applied to many case studies and successfully found previously unknown bugs. It has been adopted for research and teaching in multiple universities. More details about PAT can be found at http://www.patroot.com.
The applicant shall conduct research related to model checking techniques and security verification. Following list is the possible topics.
# Verify security systems: security protocols, web security, TPM, security device, etc.
# Software and assembly code verification.
# Code synthesis for security procotols.
# PAT optimization using techniques like distributed/parallel model checking, automated abstraction techniques (possibly domain specific), generalized symmetry reduction, etc.
The applicant will study the PAT framework, identify the suitable state reduction techniques, design/implement the techniques in PAT.
The position involves conducting basic research, developing tools, working as part of a research team, traveling, and giving presentations. The working language is English.
Candidate profile:
- A PhD in Computer Science or related areas is required.
- Expertise in Formal Methods, Model Checking technology and Security.
- Strong background in logic and discrete math.
- Strong programming skills (the language we are working with is C#).
- An established research record.
The post-doc positions are funded by large research projects in School of Computing and Temasek Laboratories, National University of Singapore.
The term is currently 3 years starting immediately and can be extended.
The salary range is around 60K-92K SGD pa (1 SGD = ~ 0.83 USD). Housing allowance may also be provided.
Interested applicants should send their CV to Dr. DONG, Jin-Song at dongjs@comp.nus.edu.sg and Dr. LIU, Yang at liuyang@comp.nus.edu.sg.
In this minor release, the update include the following:
1 Bugs for alphabet calculation are fixed in all modules.
2 Model Explorer is added in the GUI.
3 More examples are added in the CSP module.
''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>
In this release, we have the following updates:
1 The simulator drawing components are updated to the latest version of MSALG library.
2 Bug fixing and performance improvement for RTS and PRTS modules. [[RTS Module Experiments|http://www.comp.nus.edu.sg/~pat/rts]]
3 BDD performance improvement for LTS module.
4 NesC Module Improvement and new examples are added.
!''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.
After 4 months, PAT 3.4.0 is ready now. We put this release as beta version as there are some system architecture changes which affects every module. The main update of this version includes the following.
!Language Update:
# Accessing public properties/fields of C# objects using syntax like obj$property (can be read or write)
# PAT now supports channel arrays, which is a syntax suger to make the modeling easier if the channels are parameterized. The following syntax demonstrates how to use the channel array.
channel c[3] 1;
Sender(i) = c[i]!i -> Sender(i);
Receiver() = c[0]?x -> a.x -> Receiver() [] c[1]?x -> a.x -> Receiver() [] c[2]?x -> a.x -> Receiver();
System() = (||| i:{0..2}@Sender(0) ) ||| Receiver();
Note: Two or N dimentional channel array can be simulated by using 1 dimentional channel array. Hence, we don't provide syntax support for that. For example channel c[3][5] 1 is same as channel c[15] 1, and c[2][3]!4 -> Skip is same as c[2*N+3]!4 -> Skip, where N is the first dimention.
3. Channel operations
PAT provides 5 channel operations to query the buffer information of asynchronous channels: cfull, cempty, ccount, csize, cpeek. The usage of these operations follows the normal static method call, i.e., call(channel_operation, channel_name).
cfull: test whether an asynchronous channel is full or not. e.g. call(cfull, c).
cempty: test whether an asynchronous channel is empty or not. e.g. call(cempty, c).
ccount: return the number of elements in the buffer of an asynchronous channel. e.g. call(ccount, c).
csize: return the buffer size of an asynchronous channel. e.g. call(cfull, c).
cpeek: return the first element of an asynchronous channel. e.g. call(cpeek, c).
!GUI Update
#Verification window is redesigned. We remove all the options and check boxes with two selection: Admissible Behavior and Verification Engine. Admissible behavior offers the constraints on the model's behavior; Verification engine offers the possible verification algorithms (with the reduction techniques).
# A new module generator is implemented. A simple editor is avaiable for developers to testing the code. You can acutally use this generated editor project for your module development. The code is minimum and compilation speed is very fast.
# UML console supported requested by the users.
!Algorithm Update:
# BDD supports deadlock, reachability, LTL with fairness verfication now. See LTS module for the details.
# RTS module provides a new abstraction: digitalization. Users can select either zone abstraction or digitalization as the abstraction technique in verfication and simulation. For simulation, you can change the choice in the option window.
# CSP Module supports symbolic model checking using BDD
!Performance Update:
# Performance improvement for RTS and PRTS modules
# BDD performance improvement for LTS module.
# NesC Module Improvement and new examples are added.
and a lot of bug fixings...
Happy New Year! After half year's development. PAT 3.5.0 is out.
After PAT 3.5.0, .NET framework 4.0 is required to run PAT.
There are a number of new features and bugs fixing in this version as list below.
!Update of PAT 3.5.0
1 First, PAT is now running on .NET framework 4.0 in order to benefit from the newer library, particularly the parallel library in .NET 4.0.
We have done another round of code restructuring based on the new .NET framework.
2 GUI improvement
a) Simulator is supported to display all enabled events in all states or only enabled at the current active state.
b) Parsing without output parsed specification in the output window. When some model is very big, to output the string takes very long time.
This option could help to solve this problem.
3 BDD library performance improvement
4 Bug Fixing and improvement
Bug fixing for the exception due to non-boolean expression used in LTL property
Bug fixing for searching and parsing
Bug fixing for nested IndexedProcess
String Type Event in alphabet and hiding process
Comments highlighting in the assertions section of the model
!New features coming up
1 Several Multi-core model checking algorithms (Nested DFS based, Tarjon SCC search based, with fairness condition) are implemented.
These algorithms will be avaiable soon.
2 Learning based composition verification algorithms library CELL. We have implemented a number of compositional verification algorithms
and learning algorithms. This library (with source code) will be released soon.
3 New modules coming: BPEL module, Timed Automata module, UML state machine module, security module. Stay tuned.
In this minor release, the update include the following:
1 Parsers are all updated to the latest antlr library, as well as the error messages are improved.
2 In LTS module, BDD library execution error is fixed
3 Indexed Boolean logic expression is supported
e.g.
var x[3];
P = if(&& i:{0..2}@(x[i] == 0)){bingo -> Skip};
4 GUI improvement for the C# library Editor and Main GUI
5 PAT now will open the last edited documents when started
6 User Manual is updated.
!''What's new in PAT 2.9.0''
In this release, there are three new modules are released: Probability CSP Module, Orc Module and NesC module. There are a lot of changes from the user interface, language syntax and verification algorithms. So we decide to make it a beta release before it becomes stable.
''Probability CSP Module''
PCSP module extends CSP module with probabilistic behaviors. With the introducting of probability choice in the modeling, PCSP module supports the verification of deadlock, reachability and LTL properties with probability queries.
''Orc Module''
Orc module supports the modeling and verification of Orc language, developed by the UT austin university. This is a beta release. More examples and testing are needed.
''NesC module''
NesC module supports the modeling and verification of NesC language. This is a beta release. More syntax of NesC language will supported soon.
''Language Changes''
1 ''with'' clause is supported in CSP module, RTS module and PCSP module for reachability properties.
To further query about variable values, PAT allows user to find the minimum value or maximum value of some expressions in all reachable traces. The following coin changing example show how to minimize the number of coins during the reachability search.
var x = 0;
var weight = 0;
P() = if(x <= 14)
{
coin1{x = x + 1; weight =weight + 1;} -> P() [] coin2{x = x + 2; weight = weight + 1;} -> P() [] coin5{x = x + 5; weight = weight + 1;} -> P()
};
//#define goal x == 14;//
//#assert P() reaches goal with min(weight);//
2 'new' keyword is supported for the user defined data structures.
Var<HashTable> x = new HashTable(100);
3 'byte' 'short' are supported in the return type of user defined methods.
But not supported for the method parameters.
3 nested if-then-else are supported
if (cond) { P } else if (cond2) { Q }
''GUI updates''
The search depth option is removed from the verifier. We implement the shortest witness trace option to find the shortest counterexample or witness trace for deadlock, reachability and refinement checks. The shortest witness searching algorithms are based on Breadth First Search.
The simulator is added with the option of hiding tau events.
''Performance Improvement''
1 Refinement verification algorithm is updated and improved.
2 Parallel execution is simplied.
''Others''
1 User manual is updated to latest implementation.
2 Bug fixing in refinement checking algorithm
3 Bug fixing in LTL safety checking algorithm
4 LTL safety checking algorithms are implemented.
5 Examples are added for PCSP module and RTS module.
6 Parsers are improved for some error input.
PAT Student team (Li Yi, Yang Hang and Wu Huanan) won the Formal Methods Award in [[SCORE 2011|http://score-contest.org/2011/]] in Honolulu, Hawaii. There are only two awards: Formal Methods Award and Overall Award.
The system they developed is ''Transport4You, an intelligent public transportation manager'', which employs formal methods during system design, implementation, testing and verification. PAT is used as a model checker and decision maker in the project.
Statistics for SCORE 2011: 94 registrations from 48 universities in 22 countries, 55 submissions, 18 selected for the second round, 5 finalist teams invited to ICSE.
Latest stable version PAT 3.2.0 includes the stable version of the CSP module and Real-Time System Module, and a beta version of PCSP and PRTS module and Labeled Transition System (LTS) module.
For the detailed update, please refer to [[Version History]].
!''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/
1 Bug fixing for all modules for deadlock checking and divergence checking for some special cases.
2 In simulator, a Simulate Trace button is added to allow users to write a script to perform automatic simulation. After clicking it, a textbox is shown where you can writre the event trace like phil.0.0, phil.0.1, eat.0 or a, b(5), tick. Each event is seprated by comma and b(5) means you can perform b 5 times.
3 In Editior, PAT also provides another way to open the imported library directly. You can select the imported library path and then right click the button, choose "open import/include file" function to open it. This funcation can recognize absolute path, relative path to the current model file and inside lib folder of pat installation.
4 In CSP module, C++ Code generation function is improved with hardware API support and socket channel support mapping from channels.
5 For simplicity, BDD is only supporting LTS and TA module now
6 TA module performance improvement
7 our PAT.BDD library has been publish at http://www.comp.nus.edu.sg/~pat/bddlib/
8 Stop button has better responsive for LTL (with fairness) verification during the counterexample searching.
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]].
Search and Post your questions in the forum: http://patroot.forummotion.com/
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.
1 Code generation is improved and supports of more syntax for CSP module (still beta version, based on QP platform)
2 BDD support for CSP module is improved. BDD doesn't support encoding interrupt as an LTS but can encode it with compositional function.
3 Most BEEM database examples are added (work in progress)
4 RTS module bugs are fixed.
5 Monotonic engine for reachability with max or min value is added back
"Search Engine: Shortest Witness Trace using Breadth First Search with Monotonically With Value"
6 Reward calculation is supported in PRTS, and parser are improved in PRTS.
7 Indexed events are supported in all modules.
8 Macro definitions usage is improved for all modules.
Macro can take in parameters as defined below. When calling the macro, the keyword call is used. The macro expression can be any possible expression in PAT (if, local variable declarition, while, assignment).
''#define multi(i,j) i*j;''
System = if (call(multi, 3,4) >12 ) { a -> Skip } else { b -> Skip };
Note that following usage of macro definitions are also allowed in PAT, which means that macro definitions can be a fragment of code to be used in the model.
var x = 0;
var y = 0;
var z = 0;
''#define reset1 {x = 0; y = 0};''
''#define reset(i) {x = i; y = i}; ''
P = e1{z = 0; reset1} -> Skip;
Q = e2{z = 2; call(reset, 1)} -> Skip;
''9 Atomic process semantics is updated''
Since PAT 3.4.2, the semantics of atomic process changes a little bit. In the example below, before PAT 3.4.2, event a and d are enabled at the same time when process Sys starts. In PAT 3.4.2, only d is enabled because enabled atomic process has higher priority than enabled events. We did this change is to make the semantics for atomic process in real-time modules in PAT easy to express.
P = a -> atomic { b -> c -> Skip};
Q = atomic { d -> e -> f -> Skip};
Sys = P ||| Q
With this new syntax, parallel events can have priorities like a and d above.
In RTS module, atomic process can contain timing constructs now. Consider the following:
P = atomic{Wait[5]; a -> Skip} ||| Q;
Q = b -> Q;
The tau (time tick) transition geneated by by Wait[5] will have higher priority than b and the tau, and event a will be bundled together.
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]])
1 Code generation is supported for CSP module (beta version, based on QP platform)
2 BDD support for CSP module is done
3 Bitwise operator for integers is supported in all basic 5 modules: & (and), | (or) and xor (^)
4 Some BEEM database examples are added (work in progress)
5 RTS module parser update to support channel array and process parameter range
6 Parser bug fixing and macro is supported in all basic 5 modules
7 RTS non-zeno checking with zone abstraction performance improvement
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]]
Albania
Argentina
Australia
Austria
Bangladesh
Barbados
Belgium
Botswana
Brazil
Bulgaria
Cameroon
Canada
China
China, Macao
China, Taiwan
Colombia
Czech Republic
Denmark
Egypt
El Salvador
Finland
France
Germany
Haiti
Hungary
India
Indonesia
Iran
Ireland
Italy
Jamaica
Japan
Khi
Luxembourg
Macau
Macedonia
Mexico
Moldova
Netherland
New Zealand
Nigeria
Norway
Pakistan
Poland
Reunion
Romania
Russia
Senegal
Singapore
Slovak Republic
Slovakia
South Africa
South Korea
Spain
Sweden
Tunisia
Turkey
U.S.A.
Ukraine
United Arab Emirates
United Kingdom
Vietnam
Zambia
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.sutd.edu.sg/faculty/sunj/]], Assistant Professor, Singapore University of Technology and Design.
* Dr. [[LIU, Yang|http://www.ntu.edu.sg/home/yangliu/]], Assistant Professor, School of Computer Engineering, Nanyang Technological University.
* Dr. [[DONG, JinSong|http://www.comp.nus.edu.sg/~dongjs/]], Associate Professor, School of Computing, National University of Singapore.
Current Postdoc
* Dr. [[LIN Shang-Wei|http://sites.google.com/site/shangweilin/]], Compositional verification and synthesis with assume-guarantee reasoning.
* [[ZHANG Xian|http://www.comp.nus.edu.sg/~zhangxi5/]], Modeling and verifying timed systems and pervasive computing systems.
Current Ph.D Students
* ZHU, Huiquan, Model checking C# program.
* [[ZHANG Shaojie|http://www.comp.nus.edu.sg/~g0801843]], Formal verification of UML and distributed systems, event-based model checking and symmetry reduction.
* [[ZHENG Manchun|http://www.comp.nus.edu.sg/~zmanchun/]], Automatic verification of WSN software, developing [[NesC@PAT|http://www.comp.nus.edu.sg/~pat/NesC]].
* SONG Songzheng, Probabilistic model checking.
* [[TAN Tian Huat|http://www.comp.nus.edu.sg/~tianhuat/]], Verification of Web Service Composition, working on Orc Module for PAT.
* [[LIU Yan|http://www.comp.nus.edu.sg/~yanliu/]], Model checking in smart space; Reasoning and verification of context-aware applications.
* [[SHI Ling|http://www.comp.nus.edu.sg/~shiling/]], UTP Semantics of PAT modeling languages.
* GUI Lin, Software Reliability Analsysis, statistical model checking.
* [[Truong Khanh Nguyen|http://www.comp.nus.edu.sg/~nguyent9]], Symbolic model checking.
* [[BAI Guangdong|http://www.comp.nus.edu.sg/~a0091939]]
* [[JI Kun|http://www.comp.nus.edu.sg/~jikun]]
* CHEN Manman
Research Assistants
* XIAO Hao, Assembly code model checking.
* MA Junwei
Undergraduate Students
* Nguyen Chi Dat, Multi-core model checking.
Visiting Students and researchers
* SI Yuanjie, from Zhejiang University, China.
* HAO Jianye, from the Chinese University of Hong Kong.
* Pakorn Waewsawangwong, April 2011, from University of York, UK.
* Prof [[WANG Xinyu|http://www.vlis.zju.edu.cn/views/lab/ResearchTeam.aspx]], July - Sep 2011, from ZJU, China. VLS information system, software re-engineering, trustworthy software and financial information system.
Previous PAT members:
* Dr. David Sanan, Formal verification of software at source code level.
* Dr. [[CHEN Chunqing|http://www.hpl.hp.com/people/chunqing_chen/]]
* Dr. [[Étienne André|http://www-lipn.univ-paris13.fr/~andre/]], Model checking Timed systems and Parametric Timed Automata, and techniques in parameter synthesis.
* ZHANG Jiexin, Modeling and verification of Event-Grammar.
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 '.').
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.
!Research Collaborations
We own thanks to research collaborators, including [[Prof. Jun Pang|http://satoss.uni.lu/members/jun/]], [[Prof. Hai Wang|http://users.ecs.soton.ac.uk/hw/]], [[Prof. Jing Sun|http://www.cs.auckland.ac.nz/~jingsun/]], [[Prof. Wei Chen|http://www.cs.sunysb.edu/~liu/]], [[Prof. Annie Y. Liu|http://www.cs.sunysb.edu/~liu/]] and [[Prof. Geguang Pu|http://faculty.ecnu.edu.cn/pugeguang/Info_eng.html]].
We would like to thank Prof. Jing Sun, [[Prof. Hugh Anderson|http://www.comp.nus.edu.sg/~hugh/]], [[Prof. Jonathan S. Ostroff|http://www.cse.yorku.ca/~jonathan/]] for using PAT for the course teaching. Their valuable feedback made PAT more suitable for teaching.
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 [[Jim Davis|http://web.comlab.ox.ac.uk/Jim.Davies/]], 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]], professor [[Phil Brooke|https://www.scm.tees.ac.uk/p.j.brooke/]], professor [[Kenji Taguchi|http://honiden-lab.ex.nii.ac.jp/~taguchi]], professor [[Doron A. Peled|http://www.dcs.warwick.ac.uk/~doron/]] so on.
!Funding Projects
PAT is (partially) funded by the following projects:
1 ''Advanced Model Checking Systems (MOE T2, R-252-000-410-112)''
2 ''Systematic Design Methods and Tools for Developing Location Aware, Mobile and Pervasive Computing Systems (NRF-IDM, R-252-000-329-279)''
!Japanese User Group
We have special thanks to our Japanese user group, especially Hiroshi Fujimoto, Kenji Taguchi, Masaru Nagaku, Toshiyuki Fujikura.
!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>
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>
<HTML>
The following shows experimental results on embedded examples in CSP module to demonstrate the strength of PAT of handling various kinds of fairness constraints and verifying linearizability of concurrent data structure implementations.
<H2>LTL Checking under Various Kinds of Fairness Assumptions </H2>
This part shows verification statistics to show power of PAT to handle fairness in comparison to SPIN. The verified benchmark systems consist of dining philosopher problem, Milner's cyclic scheduler algorithm and Peterson's mutual exclusive algorithm.
<CENTER>
<IMG width=400 SRC="./experiments/fairness.png" BORDER="0" ALT="">
</CENTER>
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 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. The experiment data is available <A href="./experiments/fairness.zip">here</A>.
<H2>Linearizability Checking </H2>
The experiment includes a number of
concurrent data structure algorithms, including a K-valued single-writer register, a
concurrent stack, mailbox problem and scalable non-zero indicator. The following table summarizes
part of our experiments, where ‘#Processes’ means the number of interleaving
processes, ‘#Operations’ means the number of operations a process performs, ‘N/A’ means out of memory or more than two hours, and ‘Unlimited’ means a process executes operations in a loop.
<CENTER>
<IMG width=700 SRC="./experiments/linear.PNG" BORDER="0" ALT="">
</CENTER>
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 or Stack) vs. 2
processes. 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. The experiment data is available <A href="./experiments/linear_models.zip">here</A>.
<br></br>
However, the checking process still suffers from state space explosion problem.
We further address the challenge of state space reduction
of model checking linearizability by incorporating both symmetry
reduction and partial order reduction techniques. Our insight
emerged from our observation about characteristics of concurrent
object algorithms. First, concurrent objects are often designed
for a number of classes of similar threads. Such similarity or symmetry
often induces equivalent portions of the state space during
model checking process. Symmetry reduction targets at eliminating
such redundant equivalent states. Second, concurrent threads
are loosely coupled and different execution orders of transitions of
different threads may result in the same global state. Partial order
reduction is used to take advantage of this fact and restricts
model checking to explore only one of the equivalent execution
orders. Therefore, the features of concurrent data structures potentially
enable effective symmetry and partial order reductions, and
furthermore, we prove that these two techniques can be combined
for linearizability checking.
<br></br>
The new method has also been implemented in our model checker PAT
and applied to a number of real-world concurrent object algorithms,
including register-the K-valued multi-reader single-writer register, stack-a concurrent stack algorithm, buggy queue-an
incorrect queue algorithm, fixed queue-the modified correct
queue proposed, SNZI-recently-proposed complicated scalable
Non-Zero indicators espectively. For each algorithm, any
thread is constructed as a most general user to non-deterministically
execute one operation. The experiment data are presented in the following table
. In the table, ‘T’ is the total number of interleaving threads,
‘Res’ is the verification result, ‘Time’ is the running time in seconds
and ‘States’ is the number of stored states respectively for checking
with specific options (SR-symmetry reduction, POR-partial order
reduction). ‘Gain’ shows the percentage of reduced states and time
by applying two reduction techniques. ‘-’ denotes out of memory
or more than one hour.
<CENTER>
<IMG SRC="./experiments/newlinear.PNG" BORDER="0" ALT="">
</CENTER>
From the table, it is shown that symmetry reduction and/or partial
order reduction reduce both memory and time consumption as
expected, and the combination of both techniques works best in
most cases. The computational overhead stems from two aspects.
One is dependency analysis between transitions of different threads
at each exploration step for partial order reduction; the other is
checking whether any equivalent state of a visiting state has been
explored for symmetry reduction. The experiment shows that our
approach can significantly save time and space for demonstrating
absence of errors and at the same time it does not sacrifice the capability
of detecting bugs.
</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 stable version PAT 3.5.0 includes the stable version of the CSP module and Real-Time System Module, and a beta version of PCSP and PRTS module and Labeled Transition System (LTS) module.
Click [[HERE|http://register.patroot.com/Register.aspx]] 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 PAT uses 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''
For Windows OS:
* Windows Operating System: Windows XP, Vista, Windows 7 and Windows Server 2000/2003.
* .NET Framework 4.0 is needed to run PAT, which can be downloaded [[here|http://www.microsoft.com/downloads/details.aspx?FamilyId=AB99342F-5D1A-413D-8319-81DA479AB0D7&displaylang=en]].
For Linux, Mac OS and others:
* [[Mono 2.6.7|http://www.go-mono.com/mono-downloads/download.html]] or later
!''Installation''
Install PAT 3.x in Windows XP, Vista and Windows Server 2000/2003, Windows 7:
*Installing PAT is easy: run the setup file and follow the installation wizard. The following are the system requirements.
Install PAT 3.x in Linux, Unix, Mac OS or more, please follow these steps:
*You should install mono tool in your system which is freely available. Please download from [[here||http://www.go-mono.com/mono-downloads/download.html]] according to your OS. ''Note'' that libmono-winforms2.0-cil (plus its dependencies) may need be added in order to run PAT under Linux (Ubuntu).
*Download PAT 3.x. But choose the ''directly executable version'' to some place in your computer.
*In your computer, start terminal application, using the command cd to the directory where you put ''"PAT 3.exe"'';
*Type the command mono "PAT 3.exe" into terminal.(You might need to add execute permission as chmod +x "./PAT 3.exe") Bingo! You will see the GUI of our PAT.
Currently the latest mono 2.10.x has some problem on Mac, if you meet some error related to winforms, please use the mono-2.6.7 which is available [[here|http://ftp.novell.com/pub/mono/archive/2.6.7/download/]].
Note: PAT runs faster in Windows than other OS. The reason is that mono is not as fast as native .NET framework.
!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.
!''Auto Update''
Auto Update should work fine without any sepcial configuration.
However, auto updating is not avaiable for 64 bit version of PAT. We suggest you to download the latest version of 64 bit PAT from the website and install again.
![[PAT Installation FAQ]]
Experiments results in PAT are categorized by modules.
The test bed's configuration is as follows:
* Intel Xeon 4-Core CPU*2, 32 GB memory and 6 TB Hard Disk.
* Windows Server 2008 64 Bit
* PAT Version 3.2
[[CSP Module]]
[[RTS Module|http://www.comp.nus.edu.sg/~pat/rts]]
[[PCSP Module]]
[[PRTS Module]]
[[TA Module]]
[[NesC Module|http://www.comp.nus.edu.sg/~zmanchun/NesC@PAT/]]
!Experiments Comparison for different versions of PAT
[[CSP Module|http://137.132.165.220:8080/Experiment/ExperimentResult?module=CSP]]
[[PCSP Module|http://137.132.165.220:8080/Experiment/ExperimentResult?module=PCSP]]
[[RTS Module|http://137.132.165.220:8080/Experiment/ExperimentResult?module=RTS]]
[[PRTS Module|http://137.132.165.220:8080/Experiment/ExperimentResult?module=PRTS]]
[[LTS Module|http://137.132.165.220:8080/Experiment/ExperimentResult?module=LTS]]
[[TA Module|http://137.132.165.220:8080/Experiment/ExperimentResult?module=TA]]
!Experiments for ISSRE 2011 Submissions
[[Paper 121: PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers|http://www.comp.nus.edu.sg/~pat/system]]
[[Others]]
!''News''
* [[28, Dec, 2012: PAT 3.5.0 is released!]]
* [[30, July, 2012: PAT 3.4.4 is released!]]
* [[15, April, 2012: PAT 3.4.3 is released!]]
* [[4, Feb, 2012: PAT 3.4.2 is released!]]
* [[5, Jan, 2012: PAT 3.4.1 is released!]]
* [[15, Nov, 2011: PAT 3.4.1 (beta) is released!]]
* [[22, Sep, 2011: 2 Postdoc Research Fellow Positions Available on Model Checking and Security]]
* [[28, Aug, 2011: PAT 3.4 (beta) is released!]]
* [[29, May, 2011: PAT Student Team won ICSE Score Formal Methods Award]]
* [[27, April, 2011: PAT 3.3.1 is released!]]
* [[Information about NesC Module|http://www.comp.nus.edu.sg/~zmanchun/NesC@PAT/]]
* [[18, March, 2011: PAT 3.3.0 is released!]]
* [[13, March, 2011: Experiments for FSE 2011 are added!]]
* [[Old News]]
!''Introduction''
PAT is a self-contained framework for to support composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g. partial order reduction, symmetry reduction, process counter abstraction, parallel model checking. So far, PAT has ''2640+'' registered users from ''680+'' organizations in ''[[63 countries and regions]]''.
The main functionalities of PAT are listed as follows:
* User friendly editing environment (multi-document, multi-language, I18N GUI and advanced syntax editing features) for introducing models
* User friendly simulator for interactively and visually simulating system behaviors; by random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
* Easy verification for deadlock-freeness analysis, reachability analysis, state/event linear temporal logic checking (with or with fairness) and refinement checking.
* A wide range of built-in examples ranging from benchmark systems to newly developed algorithms/protocols.
We design PAT as an extensible and modularized framework, which allows user to build customized model checkers easily. We provide a library of model checking algorithms as well as the support for customizing language syntax, semantics, model checking algorithms and reduction techniques, graphic user interfaces, and domain specific abstraction techniques. Delightfully, PAT has been growing up to eleven modules today to deal with problems in different domains including Real Time Systems, Web Service Models, Probability Models, and Sensor Networks etc. In order to be state-of-the-art, we are actively developing PAT to cope with latest formal-automated system analysis techniques.
We have been using PAT to model and verify a variety of systems. Ranging from recently proposed distributed algorithms, security protocols to real-world systems like multi-lift and pacemaker systems. Previously unknown bugs have been discovered. The [[Experiments]] results show that PAT is capable of verifying systems with large number of states and outperforms the popular model checkers in some cases. We have successfully demonstrated PAT as an analyzer for process algebras in the 30th International Conference on Software Engineering (ICSE 2008), the 21st International Conference on Computer Aided Verification (CAV 2009), International Symposium on the Foundations of Software Engineering (FSE 2010), and the 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011).
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]]
''new!'' [[Videos]]
''new!'' [[Experiments]]
''new!'' [[Publications]]
[[Version History]]
[[Forum|http://patroot.forummotion.com]]
[[Bug Tracking|https://patroot.unfuddle.com/]]
[[Acknowledgment]]
[[About Us]]
<html>
<a href="http://www.facebook.com/pages/PAT-Process-Analysis-Toolkit/136690036363263" target="_TOP" style="font-family: "lucida grande",tahoma,verdana,arial,sans-serif; font-size: 11px; font-variant: normal; font-style: normal; font-weight: normal; color: #3B5998; text-decoration: none;" title="PAT: Process Analysis Toolkit">PAT on Facebook!!</a><br/><a href="http://www.facebook.com/pages/PAT-Process-Analysis-Toolkit/136690036363263" target="_TOP" title="PAT: Process Analysis Toolkit"><img src="http://badge.facebook.com/badge/136690036363263.1531.1357714309.png" width="120" height="200" style="border: 0px;" /></a><br/>
</html>
© 2007 - 2010
[[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.
* [[28, Feb, 2011: PAT 3.2.3 is released!]]
* [[21, Jan, 2011: PAT 3.2.2 is released!]]
* [[13, Jan, 2011: Experiments for FM 2011 are added!]]
* [[24, Dec, 2010: PAT 3.2.1 is released!]]
* [[11, Dec, 2010: Videos are avaiable for PCSP and NesC module!]]
* [[3, Dec, 2010: PAT 3.2.0 is released!]]
* [[06, Nov, 2010: PAT experiments are standardized and published]]
* [[13, Oct, 2010: PAT API is released!]]
* [[22, Sep, 2010: Two Posrdoc Positions on Model Checking at National University of Singapore]]
* [[2, Sep, 2010: PAT 3.2.0 (beta) is released!]]
* [[1, Aug, 2010: PAT 3.1.0 is released. PAT is cross-platform now: running on Linux, Mac OS and more!]]
* [[14, July, 2010: PAT 3.0.0 is released!]]
* [[30, May, 2010: PAT Forum is up!]]
* [[22, May, 2010: PAT 3.0.0 beta is released!]]
* [[18, March, 2010: PAT 2.9.1 is released!]]
* [[16, March, 2010: Appreciation for PAT Japanese User Group]]
* [[29, Jan, 2010: PAT 2.9.0 is released!]]
* [[02, Dec, 2009: PAT 2.8.0 is released!]]
* [[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!]]
* [[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!]]
!Experiments for FM 2011 Submissions
[[Paper 16: Developing a Model Checker for Probabilistic Real-time Hierarchical Systems|http://www.comp.nus.edu.sg/~pat/fm/prts/]]
[[Paper 23: Compositional Partial Order Reduction for Concurrent Systems|http://www.comp.nus.edu.sg/~pat/fm/cpor]]
[[Paper 40: Building Model Checkers Made Easy|http://www.comp.nus.edu.sg/~pat/fm/system]]
[[Paper 58: Formal Modeling and Verification of Ambient Intelligent System for Elderly Dementia Healthcare|http://www.comp.nus.edu.sg/~pat/fm/ai/]]
[[Paper 61: Automated Verifying Anonymity and Privacy Properties of Security Protocols|http://www.comp.nus.edu.sg/~pat/fm/security]]
[[Paper 101: On Combining State Space Reductions with Global Fairness Assumptions|http://www.comp.nus.edu.sg/~pat/fm/sym]]
!1 I can not install PAT.
Answer:
1) Make sure you have installed the .NET framework 3.5.
2) Make sure the installation file is correctedly downloaded: "PAT3.Setup.XXX.msi". Some users accidentally rename the installation file with extra .exe in the end.
3) The last remedy is to download direct executable of PAT and run it directly without installation.
!2: Cannot start PAT 3.exe on mono
Answer: If the error message informs that assembly System.Windows.Forms is missing, please get the packages libmono-winforms1.0-cil and libmono-winforms2.0-cil.
If you get "Could not get XIM" error, one way you could do is to set the environment variable as "export MONO_WINFORMS_XIM_STYLE=disabled".
!3 I can not start the simulator.
Answer:
Please make sure you have [[this DLL|System.Core.dll]] under your installation folder.
<HTML>
The following experiments are used to indicate what the performance that PAT
has in probabilistic model checking. The models we use include several
protocols:
model ME describes a probabilistic solution to N-process mutual exclusion
problem; model RC is a shared coin protocol of the randomized consensus
algorithm; Model DP is the probabilistic N-dining philosophers under fairness
and Model CS is the IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with
Collision
Detection) protocol. Then we check the maximal probability(pmax) or minimal
probability(pmin) that the model could satisfy the desired properties and
compare the result with PRISM. <BR></br>
<caption align="center">Table 1. Experiments on modeling</caption>
<CENTER>
<IMG width=600 name="Table 1. Experiments on modeling" SRC="./experiments/PCSP_modeling.png" BORDER="0" ALT="">
</CENTER>
</br>
<caption align="center">Table 2. Experiments on refinement checking</caption>
<CENTER>
<IMG width=600 name="Table 2. Experiments on refinement checking" SRC="./experiments/PCSP_Refinement1.png" BORDER="0" ALT="">
</CENTER>
</br>
<caption align="center">Table 3. Experiments on LTL checking</caption>
<CENTER>
<IMG width=600 name="Table 3. Experiments on LTL checking" SRC="./experiments/PCSP_LTL.png" BORDER="0" ALT="">
</CENTER>
From Table 3, it is obvious that PAT has much good performance in probabilistic
model checking. Although the states and verification time increase quickly
when the parameter becomes larger and larger, PAT always has a comparable and
even better output compared with PRISM. Because our algorithm uses safety
recognition, the LTL which is safety or co-safety could be verified quite
fast. For example, in the RC(N=6, K=6) case, the co-safety(1) takes PAT 6s but
takes PRISM almost half an hour; and the co-safety(2) property cannot be
verified in PRISM within 10000 iteration but in PAT we could get the result in
several minutes. Even for liveness property, PAT could have a better
performance because our modeling language could guarantee smaller state space
in the same model compared with PRISM. However, PRISM could handle more states
per seconds, which could be indicated by the deadlock checking in the table,
so we are still improving our algorithm and data structure in this module, in
order to get better performance. The experiment data is available <A href="./experiments/PCSP_experiments.zip">here</A>.
</HTML>
<HTML>
The example we use in PRTS module is a multi-lift system. The motivation is an
interesting phenomena: sometimes a user has requested a service in multi-lift
system, but a lift traveling in the same direction passes by that user and the
user must wait for another lift to serve it. This is actually because the
request assignment algorithm in the system and some other unpredictable
reasons such as a lift could be occupied arbitrary time because of other
users. We use PAT to model this complicated system which combines concurrency,
real-time and probability, and 2 methods of assigning the requests are
modeled: one is choosing the nearest lift and the other is choosing an
arbitrary one.
<CENTER>
<IMG width=600 SRC="./experiments/PRTS.png" BORDER="0" ALT="" >
</CENTER>
Because of the complexity of this system, now PAT could just handle 2 lifts,
otherwise there will be state explosion. But we could still get some
reasonable results from this table. Firstly, the more users are there, the
higher probability that some users will be passed by. Secondly, if we use
nearest lift assignment, we could expect a smaller probability that such bad
behavior could happen, which could be found in Lift_223_nearest and
Lift_223_random cases. There are many optimization could be implemented in
PAT, so we can expect better and better performance in this module. The experiment data is available <A href="./experiments/PRTS_experiments.zip">here</A>.
</HTML>
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.
!When you cite PAT, please use our CAV 09 paper: PAT: Towards Flexible Verification under Fairness. ([[Bib|publications/bibs.html#cav09]])
!Selected Publications
# Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André. ''[[Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP|http://doi.acm.org/10.1145/2430536.2430537]]''. The ACM Transactions on Software Engineering and Methodology (TOSEM), 22(1):3:1-3:29, 2013. ([[Pdf|publications/tosem13.pdf]], [[Bib|publications/bibs.html#tosem13]])
# Tian Huat Tan, Etienne Andre, Jun Sun, Yang Liu, Jin Song Dong and Manman Chen. ''Dynamic Synthesis of Local Time Requirement for Service Composition''. The 35th International Conference on Software Engineering (ICSE 2013), San Francisco, CA, USA, May 18 - 26, 2013 (Accepted).
# Guangdong Bai, Jike Lei, Guozhu Meng, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu, and Jin Song Dong. ''[[AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations|http://www.internetsociety.org/sites/default/files/04_4_0.pdf]]''. Proceedings of the Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, February 24-27, 2013. ([[Pdf|publications/NDSS13.pdf]], [[Bib|publications/bibs.html#ndss13]], [[Slides|publications/NDSS13 slide.pdf]])# Guangdong Bai, Jike Lei, Guozhu Meng, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu, and Jin Song Dong. ''AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations''. Proceedings of the Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, February 24-27, 2013. ([[Pdf|publications/NDSS13.pdf]])
# Yang Liu, Wei Chen, Yanghong A. Liu, S.J. Zhang, J. Sun and Jin Song Dong. ''Verifying Linearizability via Optimized Refinement Checking'', IEEE Transactions on Software Engineering (TSE). (Accepted)
# Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong and Yan Liu. ''[[Improved BDD-based Discrete Analysis of Timed Systems|http://dx.doi.org/10.1007/978-3-642-32759-9_28]]''. The 18th International Symposium on Formal Methods (FM 2012), pages 326-340, Paris, France, Auguest 27 - 31, 2012. ([[Pdf|publications/fm12.pdf]], [[Bib|publications/bibs.html#fm12a]], [[Slides|publications/FM12 slide.pdf]])
# Shaojie Zhang, Jun Sun, Jun Pang, Yang Liu and Jin Song Dong. ''[[On Combining State Space Reductions with Global Fairness Assumptions|http://www.springerlink.com/content/n24745221p6q2321/]]''. The 17th International Symposium on Formal Methods (FM 2011), pages 432 - 447, Lero, Limerick, Ireland, June 20 - 24, 2011. ([[Pdf|publications/fm11paper.pdf]], [[Bib|publications/bibs.html#fm11]], [[Slides|publications/fm11 slides.pdf]])
# Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu and Jin Song Dong. ''[[Fair Model Checking with Process Counter Abstraction|http://www.springerlink.com/content/g9x418h563240884/]]''. The 16th International Symposium on Formal Methods (FM 2009). pages 123 - 139, Eindhoven, the Netherlands, November, 2009. ([[Pdf|publications/fm09Counter.pdf]], [[Bib|publications/bibs.html#fm09b]], [[Slides|publications/fm09Counter.zip]])
# Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. ''[[Model Checking Lineariability via Refinement|http://www.springerlink.com/content/5l72546040254p24/]]''. The 16th International Symposium on Formal Methods (FM 2009). pages 321-337, Eindhoven, the Netherlands, November, 2009. ([[Pdf|publications/linearizability.pdf]], [[Bib|publications/bibs.html#fm09a]], [[Slides|publications/linearizability.ppt]])
# Jun Sun, Yang Liu, Jin Song Dong and Jun Pang. ''[[PAT: Towards Flexible Verification under Fairness|http://www.springerlink.com/content/0321170v636j1853/]]''. The 21th International Conference on Computer Aided Verification (CAV 2009), pages 709-714, Grenoble, France, June, 2009. ([[Pdf|publications/cav09.pdf]], [[Bib|publications/bibs.html#cav09]], [[Slides|publications/cav-slides.ppt]]).
!All Publications
!2013
# Shuang Liu, Yang Liu, Jun Sun, Manchun Zheng, Bimlesh Wadhwa and Jin Song Dong. ''USMMC: A Self-Contained Model Checker for UML State Machines''. The 9th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2013) , August 21–23, 2013, Saint Petersburg, Russia. (Accepted).
# Jianan Hao, Yang Liu, Wentong Cai, Guangdong Bai and Jun Sun. ''vTRUST: A Formal Modeling and Verification Framework for Virtualization Systems''. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 - Nov 1, Queenstown, New Zealand. (Accepted).
# Yuanjie Si, Jun Sun, Yang Liu and Ting Wang. ''Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction''. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 - Nov 1, Queenstown, New Zealand. (Accepted).
# Manman Chen, Tian Huat Tan, Jun Sun and Yang Liu. ''Verification of Functional and Non-functional Requirements of Web Service Composition''. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 - Nov 1, Queenstown, New Zealand. (Accepted).
# Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong and Shengchao Qin. ''A UTP Semantics for Communicating Processes with Shared Variables''. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 - Nov 1, Queenstown, New Zealand. (Accepted).
# Kun Ji, Yang Liu, Shang-Wei Lin, Jun Sun, Jin Song Dong and Truong Khanh Nguyen. ''CELL: A Compositional Verification Framework''. The 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013) , October 15 - 18, 2013, Hanoi, Vietnam. (Accepted).
# Takahiro Ando, Hirokazu Yatsu, Weiqiang Kong, Kenji Hisazumi, and Akira Fukuda. Formalization and Model Checking of SysML State Machine Diagrams by CSP#. In: The 2013 International Conference on Computational Science and Its Applications (ICCSA 2013), Ho Chi Minh City, Vietnam, June 24-27, 2013. (accepted to be published)
# Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang. ''Towards verification of computation orchestration''. Formal Aspects of Computing (FAOC). (Accepted)
# Lin Gui, Jun Sun, Yang Liu, Yuanjie Si, Jinsong Dong and Xinyu Wang. ''Combining Model Checking and Testing with an Application to Reliability Prediction and Distribution''. The International Symposium in Software Testing and Analysis (ISSTA 2013) , Lugano, Switzerland, 15-20 July 2013. (Accepted).
# Shuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa and Jin Song Dong. ''[[A Formal Semantics for the Complete Syntax of UML State Machines with Communications|http://dx.doi.org/10.1007/978-3-642-38613-8_23]]''. The 10th International Conference on integrated Formal Methods (iFM 2013), June 10 - 14, Turku, Finland, 2013. ([[Pdf|publications/ifm13 uml.pdf]], [[Bib|publications/bibs.html#ifm13b]], [[Slides|publications/ifm13 uml.pptx]])
# Songzheng Song, Lin Gui, Jun Sun, Yang Liu and Jin Song Dong. ''Improved Reachability Analysis in DTMC via Divide and Conquer|http://dx.doi.org/10.1007/978-3-642-38613-8_12''. The 10th International Conference on integrated Formal Methods (iFM 2013), Turku, Finland, June 10 - 14, 2013. ([[Pdf|publications/ifm13 dtmc.pdf]], [[Bib|publications/bibs.html#ifm13a]], [[Slides|publications/ifm13 dtmc_slide.pdf]])
# Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André. ''[[Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP|http://doi.acm.org/10.1145/2430536.2430537]]''. The ACM Transactions on Software Engineering and Methodology (TOSEM), 22(1):3:1-3:29, 2013. ([[Pdf|publications/tosem13.pdf]], [[Bib|publications/bibs.html#tosem13]])
# Étienne André, Yang Liu, Jun Sun, Jin Song Dong and Shang-Wei Lin. ''Parameter Synthesis for Hierarchical Concurrent Real-Time Systems''. The 25th International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia, July 13 - 19, 2013 (Accepted).
# Jin Song Dong, Jun Sun and Yang Liu. ''Build Your Own Model Checker in One Month''. The 35th International Conference on Software Engineering (ICSE 2013), Tutorial, San Francisco, CA, USA, May 18th - 26th, 2013 ([[Pdf|publications/ICSE13 tutorial.pdf]]).
# Tian Huat Tan, Etienne Andre, Jun Sun, Yang Liu, Jin Song Dong and Manman Chen. ''Dynamic Synthesis of Local Time Requirement for Service Composition''. The 35th International Conference on Software Engineering (ICSE 2013), San Francisco, CA, USA, May 18 - 26, 2013 (Accepted).
# Guangdong Bai, Jike Lei, Guozhu Meng, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu, and Jin Song Dong. ''[[AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations|http://www.internetsociety.org/sites/default/files/04_4_0.pdf]]''. Proceedings of the Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, February 24-27, 2013. ([[Pdf|publications/NDSS13.pdf]], [[Bib|publications/bibs.html#ndss13]], [[Slides|publications/NDSS13 slide.pdf]])
# Yang Liu, Wei Chen, Yanghong A. Liu, S.J. Zhang, J. Sun and Jin Song Dong. ''Verifying Linearizability via Optimized Refinement Checking'', IEEE Transactions on Software Engineering (TSE). (Accepted)
# Manchun Zheng, David Sanán, Jun Sun, Yang Liu, Jin Song Dong and Yu Gu. ''[[State Space Reduction for Sensor Networks using Two-level Partial Order Reduction|http://dx.doi.org/10.1007/978-3-642-35873-9_30]]''. The 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2013), pages 515-535, Rome, Italy, January 20-22, 2013. ([[Pdf|publications/vmcai13.pdf]], [[Bib|publications/bibs.html#vmcai13]], [[Slides|publications/vmcai13_slide.pdf]])
!2012
# Suman Roy, Sidharth Bihary and Jose Alfonso Corso Laos. ''A Conformance Checker Tool CSPConCheck''. The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012), pages 159-163, Bangalore, India, September 24 - 27, 2012.
# Oğuzcan OĞUZ, Jan F. BROENINK and Angelika MADER. ''Schedulability Analysis of Timed CSP Models Using the PAT Model Checker''. The 34th Communicating Process Architectures Conference, CPA 2012, organised under the auspices of WoTUG, Dundee, Scotland, August 26 - 29, 2012.
# Vwen Yen Lee, Yan Liu, Xian Zhang, Clifton Phua, Kelvin Sim, Jiaqi Zhu, Jit Biswas, Jin Song Dong, Mounir Mokhtari. ''ACARP: Auto Correct Activity Recognition Rules Using Process Analysis Toolkit (PAT)''. The 10th International Conference on Smart Homes and Health Telematics, ICOST 2012, Artiminio, Italy, June 12 - 15, 2012.
# Jie Xin Zhang, Yang Liu, Jing Sun, Jin Song Dong and Jun Sun. ''[[Model Checking Software Architecture Design|http://doi.ieeecomputersociety.org/10.1109/HASE.2012.12]]''. The 14th International Symposium on High-Assurance Systems Engineering (HASE 2012), pages 193-200, Omaha, USA, October 25 -27, 2012 ([[Pdf|publications/hase12.pdf]], [[Bib|publications/bibs.html#hase12]]).
# Jiexin Zhang, Yang Liu, Mikhail Auguston, Jun Sun and Jin Song Dong. ''Using Monterey Phoenix to Formalize and Verify System Architectures''. The 19th Asia-Pacific Software Engineering Conference (APSEC 2012), Hong Kong, December 4 - 7, 2012 ([[Pdf|publications/apsec12.pdf]]).
# Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang and Shanping Li. ''[[More Anti-Chain Based Refinement Checking|http://dx.doi.org/10.1007/978-3-642-34281-3_26]]''. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 364-380, Kyoto, Japan, November 12 - 16, 2012. ([[Pdf|publications/icfem12 anti-chain.pdf]], [[Bib|publications/bibs.html#icfem12d]])
# Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun and Jin Song Dong. ''[[Automatic Generation of Provably Correct Embedded Systems|http://dx.doi.org/10.1007/978-3-642-34281-3_17]]''. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 214-229, Kyoto, Japan, November 12 - 16, 2012. ([[Pdf|publications/icfem12 generation.pdf]], [[Bib|publications/bibs.html#icfem12c]], [[Slides|publications/icfem12 generation_slide.pdf]])
# Ling Shi, Yang Liu, Jun Sun, Jin Song Dong and Gustavo Carvalho. ''[[An Analytical and Experimental Comparison of CSP Extensions and Tools|http://dx.doi.org/10.1007/978-3-642-34281-3_27]]''. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 381-397, Kyoto, Japan, November 12 - 16, 2012. ([[Pdf|publications/icfem12 comparison.pdf]], [[Bib|publications/bibs.html#icfem12b]], [[Slides|publications/icfem12 comparison_slide.pdf]])
# Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. ''[[Symbolic Model-Checking of Stateful Timed CSP using BDD and Digitization|http://dx.doi.org/10.1007/978-3-642-34281-3_28]]''. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 398-413, Kyoto, Japan, November 12 - 16, 2012. ([[Pdf|publications/icfem12 symbolic.pdf]], [[Bib|publications/bibs.html#icfem12a]])
# Yi Li, Jing Sun, Jin Song Dong, Yang Liu and Jun Sun. ''Planning as Model Checking Tasks''. The 35th Annual IEEE Software Engineering Workshop (SEW-35), Heraclion, Crete, Greece, Oct 12 - 13, 2012 (Accepted).
# Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Liu Gui, Jin Song Dong and Ho-Fung Leung. ''[[Probabilistic Model Checking Multi-agent Behaviors in Dispersion Games Using Counter Abstraction|http://dx.doi.org/10.1007/978-3-642-32729-2_2]]''. The 15th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2012), pages 16-30, Kuching, Sarawak, Malaysia, September 3 - 7, 2012. ([[Pdf|publications/PRIMA12.pdf]], [[Bib|publications/bibs.html#prima12]])
# Chunqing Chen, Jun Sun, Yang Liu, Jin Song Dong and Manchun Zheng. ''[[Formal Modeling and Validation of Stateflow Diagrams|http://www.springerlink.com/content/h26l643g01546161]]''. The International Journal on Software Tools for Technology Transfer (STTT), 14:653-671, 2012. ([[Pdf|publications/sttt12.pdf]], [[Bib|publications/bibs.html#sttt12]])
# Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong and Étienne André. ''[[Automatic Compositional Verification of Timed Systems|http://dx.doi.org/10.1007/978-3-642-32759-9_24]]''. The 18th International Symposium on Formal Methods (FM 2012), pages 272-276, Paris, France, Auguest 27 - 31, 2012. ([[Pdf|publications/fm12 tool.pdf]], [[Bib|publications/bibs.html#fm12b]], [[Slides|publications/FM12_Slides_short.pdf]])
# Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong and Yan Liu. ''[[Improved BDD-based Discrete Analysis of Timed Systems|http://dx.doi.org/10.1007/978-3-642-32759-9_28]]''. The 18th International Symposium on Formal Methods (FM 2012), pages 326-340, Paris, France, Auguest 27 - 31, 2012. ([[Pdf|publications/fm12.pdf]], [[Bib|publications/bibs.html#fm12a]], [[Slides|publications/FM12 slide.pdf]])
# Yan Liu, Xian Zhang, Yang Liu, Jun Sun, Jin Song Dong, Jit Biswas and Mounir Mokhtari. ''[[Formal Analysis of Pervasive Computing Systems|http://doi.ieeecomputersociety.org/10.1109/ICECCS.2012.19]]''. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), pages 169-178, Paris, France, July 18 - 20, 2012. ([[Pdf|publications/ICECCS12 pervasive.pdf]], [[Bib|publications/bibs.html#iceccs12c]], [[Slides|publications/ICECCS12 pervasive_slide.pdf]])
# Yi Li, Jing Sun, Jin Song Dong and Yang Liu. ''[[Translating PDDL into CSP# - the PAT Approach|http://doi.ieeecomputersociety.org/10.1109/ICECCS.2012.41]]''. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), pages 240-249, Paris, France, July 18 - 20, 2012. ([[Pdf|publications/ICECCS12 PDDL.pdf]], [[Bib|publications/bibs.html#iceccs12b]])
# Étienne André, Yang Liu, Jun Sun and Jin Song Dong. ''[[Parameter Synthesis for Hierarchical Concurrent Real-Time Systems|http://doi.ieeecomputersociety.org/10.1109/ICECCS.2012.29]]''. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), pages 253-262, Paris, France, July 18 - 20, 2012. ([[Pdf|http://www-lipn.univ-paris13.fr/~andre/documents/parameter-synthesis-for-hierarchical-concurrent-real-time-systems.pdf]], [[Bib|publications/bibs.html#iceccs12a]], [[Slides|http://www-lipn.univ-paris13.fr/~andre/documents/2012-07-20-ICECCS.pdf]])
# Songzheng Song, Jun Sun, Yang Liu, and Jin Song Dong. ''[[A Model Checker for Hierarchical Probabilistic Real-time Systems|http://dx.doi.org/10.1007/978-3-642-31424-7_53]]''. The 24th International Conference on Computer Aided Verification (CAV 2012), pages 705-711, Berkeley, California, USA, July 7-13, 2012. ([[Pdf|publications/cav12.pdf]], [[Bib|publications/bibs.html#cav12]], [[Slides|publications/cav12_slide.pdf]])
# GuanJun Liu, Jun Sun, Yang Liu, and Jin Song Dong. ''[[Complexity of the Soundness Problem of Bounded Workflow Nets|http://dx.doi.org/10.1007/978-3-642-31131-4_6]]''. The 33rd International Conference on Application and Theory of Petri Nets and Concurrency (PN 2012), pages 92-107, Hamburg, Germany, June 25-29, 2012. ([[Pdf|publications/pn12.pdf]], [[Bib|publications/bibs.html#pn12]], [[Slides|publications/pn12_slide.pdf]])
# Songzheng Song, Jianye Hao, Yang Liu, Jun Sun, Ho-Fung Leung, and Jin Song Dong. ''[[Analyzing Multi-agent Systems with Probabilistic Model Checking Approach|http://dx.doi.org/10.1109/ICSE.2012.6227085]]''. The 34th International Conference on Software Engineering (ICSE 2012), New Ideas and Emerging Results (NIER), pages 1337-1340, Zurich, Switzerland, June 2 - 9, 2012. ([[Pdf|publications/ICSE12 PMA.pdf]], [[Bib|publications/bibs.html#icse12]], [[Slides|publications/ICSE2012_slide.pdf]])
# Luu Anh Tuan, Jun Sun, Yang Liu, Jin Song Dong, Xiaohong Li, and Quan Thanh Tho. ''[[SEVE: Automatic Tool for Verification of Security Protocols|http://dx.doi.org/10.1007/s11704-012-2903-3]]''. Frontiers of Computer Science, Special Issue on Formal Engineering Method, 6(1):57-75, 2012. ([[Bib|publications/bibs.html#focsc12]])
# Nguyen Chi Dat. ''Multi-Core Model Checking''. FYP Report, 2012. ([[Pdf|publications/fypreport12.pdf]])
# Xian Zhang. ''Verification of Timed Process Algebra and Beyond''. Phd Thesis, 2012. ([[Pdf|publications/ZhangXian.pdf]])
!2011
# Yi Li. ''Model Checking as Planning and Service''. FYP Report, 2011. ([[Pdf|publications/fypreport11.pdf]])
# Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. ''[[A Symbolic Model Checking Framework for Hierarchical Systems|http://dx.doi.org/10.1109/ASE.2011.6100143]]''. The 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011), pages 633-636, Lawrence, Kan., USA, Nov 6 - 11, 2011. ([[Pdf|publications/ase11.pdf]], [[Bib|publications/bibs.html#ase11]], [[Slides|publications/ase11poster.pptx]])
# Manchun Zheng, Jun Sun, David Sanán, Yang Liu, Jin Song Dong, Yu Gu. ''[[Demo: Towards Bug-free Implementations for Wireless Sensor Networks|http://doi.acm.org/10.1145/2070942.2071013]]''. The 9th ACM Conference on Embedded Networked Sensor Systems (Sensys 2011), pages 407-408, Seattle, WA, USA, Nov 1 - 4, 2011. ([[Pdf|publications/sensys11.pdf]], [[Bib|publications/bibs.html#sensys11]]).
# Yang Liu, Jun Sun and Jin Song Dong. ''[[PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers|http://doi.ieeecomputersociety.org/10.1109/ISSRE.2011.19]]''. The 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011), pages 190-199, Hiroshima, Japan, Nov 29 - Dec 2, 2011. ([[Pdf|publications/issre2011.pdf]], [[Bib|publications/bibs.html#issre11]], [[Slides|publications/ISSRE 11 Talk.pptx]])
# Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, and Yang Liu. ''[[Efficient Algorithm for Learning Event-Recording Automata|http://dx.doi.org/10.1007/978-3-642-24372-1_35]]''. The 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), pages 463-472, Taipei, Taiwan, October 11 - 14, 2011. ([[Pdf|publications/atva2011.pdf]], [[Bib|http://www-lipn.univ-paris13.fr/~andre/documents/LADSL11.bib]], [[Slides|publications/atva2011_slide.pdf]])
# Zhenchang Xing, Jun Sun, Yang Liu and Jin Song Dong. ''[[Differencing Labeled Transition Systems|http://dx.doi.org/10.1007/978-3-642-24559-6_36]]''. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 537-552, Durham, United Kingdom, October 25-28, 2011. ([[Pdf|publications/icfem2011_specdiff.pdf]], [[Bid|publications/bibs.html#icfem11d]], [[Slides|publications/icfem2011_specdiff.pptx]])
# Jun Sun, Yang Liu, Songzheng Song and Jin Song Dong. ''[[PRTS: An Approach for Model Checking Probabilistic Real-time Hierarchical Systems|http://dx.doi.org/10.1007/978-3-642-24559-6_12]]''. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 147-162, Durham, United Kingdom, October 25-28, 2011. ([[Pdf|publications/timed-ICFEM 2011.pdf]], [[Bid|publications/bibs.html#icfem11c]], [[Slides|publications/ICFEM2011 PRTS.pdf]])
# Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong and Yu Gu. ''[[Towards a Model Checker for NesC and Wireless Sensor Networks|http://dx.doi.org/10.1007/978-3-642-24559-6_26]]''. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 372-387, Durham, United Kingdom, October 25-28, 2011. ([[Pdf|publications/ICFEM11ZhengSLDG.pdf]], [[Bid|publications/bibs.html#icfem11b]], [[Slides|publications/icfem11nec.ppt]])
# Tian Huat Tan, Yang Liu, Jun Sun and Jin Song Dong. ''[[Verification of Computation Orchestration System with Compositional Partial Order Reduction|http://dx.doi.org/10.1007/978-3-642-24559-6_9]]''. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 98-114, Durham, United Kingdom, October 25-28, 2011. ([[Pdf|publications/icfem11orc.pdf]], [[Bid|publications/bibs.html#icfem11a]], [[Slides|publications/ICFEM2011 Orc.pdf]])
# Shaojie Zhang, Jun Sun, Jun Pang, Yang Liu and Jin Song Dong. ''[[On Combining State Space Reductions with Global Fairness Assumptions|http://www.springerlink.com/content/n24745221p6q2321/]]''. The 17th International Symposium on Formal Methods (FM 2011), pages 432 - 447, Lero, Limerick, Ireland, June 20 - 24, 2011. ([[Pdf|publications/fm11paper.pdf]], [[Bib|publications/bibs.html#fm11]], [[Slides|publications/fm11 slides.pdf]])
# Jin Song Dong, Jun Sun and Yang Liu. ''Tutorial: Developing Your Own Model Checker in One Month''. The 17th International Symposium on Formal Methods (FM 2011), Lero, Limerick, Ireland, June 20 - 24, 2011. ([[Slides|publications/research.pptx]])
!2010
# Ka Lok Man and Tomas Krilavičius. ''Research on Process Algebraic Analysis Tools for Electronic System Design''. Intelligent Automation and Computer Engineering, Volume 52, 415 - 427, 2010.
# Jun Sun, Yang Liu, Jin Song Dong, Geguang Pu and Tian Huat Tan. ''[[Model-based Methods for Linking Web Service Choreography and Orchestration|http://portal.acm.org/citation.cfm?id=1931918]]''. The 17th Asia Pacific Software Engineering Conference (APSEC 2010), pages 166-175, Sydney, Australia, 30 November – 3 December 2010. ([[Pdf|publications/apsec10.pdf]], [[Bib|publications/bibs.html#apsec10]], [[Slides|publications/WebService.ppt]])
# Yang Liu, Jun Sun and Jin Song Dong. ''[[Analyzing Hierarchical Complex Real-time Systems|http://portal.acm.org/citation.cfm?id=1882350]]''. The ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2010), pages 365-366, Santa Fe, New Mexico, USA, 7-11 November 2010. ([[Pdf|publications/fse10.pdf]], [[Bib|publications/bibs.html#fse10]], [[Slides|publications/FSE-talks.zip]])
# Jun Sun, Yang Liu and Bin Cheng. ''[[Model Checking a Model Checker: A Code Contract Combined Approach|http://www.springerlink.com/content/41v1855413800574/]]''. The 12th International Conference on Formal Engineering Methods (ICFEM 2010), pages 518-533, Shang Hai, China, 16-19 November 2010. ([[Pdf|publications/icfem10b.pdf]], [[Bib|publications/bibs.html#icfem10b]], [[Slides|publications/icfem2010.zip]])
# Yang Liu, Jun Sun, Jin Song Dong. ''[[Developing Model Checkers Using PAT|http://www.springerlink.com/content/80pg03408j416941/]]''. 8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010), pages 371-377, Singapore, 2010. ([[Pdf|publications/atva10.pdf]], [[Bib|publications/bibs.html#atva10]])
# Jun Sun, Songzheng Song and Yang Liu. ''[[Model Checking Hierarchical Probabilistic Systems|http://www.springerlink.com/content/a472125388x12552/]]''. The 12th International Conference on Formal Engineering Methods (ICFEM 2010), pages 388-403, Shang Hai, China, 16-19 November 2010. ([[Pdf|publications/icfem10a.pdf]], [[Bib|publications/bibs.html#icfem10a]], [[Slides|publications/ICFEM 2010.pptx]])
# Zhenchang Xing, Jun Sun, Yang Liu and Jin Song Dong. ''[[SpecDiff: Debugging Formal Specifications|http://portal.acm.org/citation.cfm?id=1859072]]''. The 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), pages 353-354, Antwerp, Belgium, 20-24 September 2010. ([[Pdf|publications/ase43te.pdf]], [[Bib|publications/bibs.html#ase10]], [[Slides|publications/ase10.zip]])
# Luu Anh Tuan. ''[[Modeling and Verifying Security Protocols Using PAT Approach|http://doi.ieeecomputersociety.org/10.1109/SSIRI-C.2010.34]]''. The 1st International Workshop on Model Checking Secure and Reliable Systems (MoCSeRS 2010). pages 157-164, Singapore, June, 2010. ([[Pdf|publications/Modeling and verifying security protocols using PAT approach.pdf]], [[Bib|publications/bibs.html#MoCSeRS10c]], [[Slides|publications/Security presentation.pptx]])
# Ling Shi and Yan Liu. ''[[Modeling and Verification of Transmission Protocols: A Case Study on CSMA/CD Protocol|http://doi.ieeecomputersociety.org/10.1109/SSIRI-C.2010.33]]''. The 1st International Workshop on Model Checking Secure and Reliable Systems (MoCSeRS 2010). pages 143-149, Singapore, June, 2010. ([[Pdf|publications/mocser10CSMACD.pdf]], [[Bib|publications/bibs.html#MoCSeRS10b]], [[Slides|publications/mocser10CSMACD slide.pdf]])
# Nguyen Truong Khanh, Quan Thanh Tho. ''[[Using Multi Decision Diagram in Model Checking|http://www.computer.org/portal/web/csdl/doi/10.1109/SSIRI-C.2010.31]]''. The 1st International Workshop on Model Checking Secure and Reliable Systems (MoCSeRS 2010). pages 126-129, Singapore, June, 2010. ([[Pdf|publications/SSIRI 2010-Khanh.pdf]], [[Bib|publications/bibs.html#MoCSeRS10a]], [[Slides|publications/]])
# Man Chun Zheng. ''[[An Automatic Approach to Verify Sensor Network Systems.|http://www.computer.org/portal/web/csdl/doi/10.1109/SSIRI-C.2010.12]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 7-12, Singapore, June, 2010. ([[Pdf|publications/ssiri2010Nec.pdf]], [[Bib|publications/bibs.html#ssiri10f]], [[Slides|publications/Automatic Verification of Sensor Network Systems.pptx]])
# Shao Jie Zhang, Yang Liu. ''[[An Automatic Approach to Model Checking UML State Machines|http://www.computer.org/portal/web/csdl/doi/10.1109/SSIRI-C.2010.11]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 1-6, Singapore, June, 2010. ([[Pdf|publications/ssiri10uml.pdf]], [[Bib|publications/bibs.html#ssiri10e]], [[Slides|publications/umlslides.pdf]])
# Songzheng Song.''[[An Efficient Method of Probabilistic Model Checking|http://doi.ieeecomputersociety.org/10.1109/SSIRI-C.2010.14]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 24-25, Singapore, June, 2010. ([[Pdf|publications/]], [[Bib|publications/bibs.html#ssiri10d]], [[Slides|publications/]])
# Tian Huat Tan. ''[[Towards Verification of a Service Orchestration Language |http://www.computer.org/portal/web/csdl/doi/10.1109/SSIRI-C.2010.20]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 36-37, Singapore, June, 2010. ([[Pdf|publications/ssiri2010Orc.pdf]], [[Bib|publications/bibs.html#ssiri10c]], [[Slides|publications/ssiri 2010Orcslide.pdf]])
# Huiquan Zhu. ''[[Model Checking C# Code: A Translation Approach|http://doi.ieeecomputersociety.org/10.1109/SSIRI-C.2010.17]]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 30-31, Singapore, June, 2010. ([[Pdf|publications/ssiriHuiquan.pdf]], [[Bib|publications/bibs.html#ssiri10b]], [[Slides|publications/Model_Checking_C_Code_A_Translation_Approach.ppt]])
# Luu Anh Tuan, Man Chun Zheng, Quan Thanh Tho. ''[[Modeling and Verification of Safety Critical Systems: A Case Study on Pacemaker|http://www.computer.org/portal/web/csdl/doi/10.1109/SSIRI.2010.28]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 23-32, Singapore, June, 2010. ([[Pdf|publications/ssiri10_pacemaker.pdf]], [[Bib|publications/bibs.html#ssiri10a]])
# Shaojie Zhang and Yang Liu. ''[[Model Checking a Lazy Concurrent List-Based Set Algorithm|http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5502856]]''. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 43-52, Singapore, June, 2010. ''Best Paper Awards'' ([[Pdf|publications/SSIRI2010.pdf]], [[Bib|publications/bibs.html#ssiri10]], [[Slides|publications/ssiriShaojie.pdf]])
# Yang Liu. ''[[Model Checking Concurrent and Real-time Systems: the PAT Approach|http://www.ntu.edu.sg/home/yangliu/thesis/thesis.pdf]]''. PhD thesis, May, 2010.
!2009
# Man, K.L., Krilavicius, T., Leung, H.L.. ''Case studies with Process Analysis Toolkit (PAT)''. International SoC Design Conference (ISOCC), 2009.
# Yang Liu, Jun Sun and Jin Song Dong. ''[[Scalable Multi-Core Model Checking Fairness Enhanced Systems|http://www.springerlink.com/content/t20246537n4ruw1w/]]''. 11th International Conference on Formal Engineering Methods (ICFEM 2009). pages 426-445, Rio de Janeiro, Brazil, December, 2009. ([[Pdf|publications/ICFEM09b.pdf]], [[Bib|publications/bibs.html#icfem09b]], [[Slides|publications/PAT-Presentation-ICFEM2009b.pptx]])
# Jun Sun, Yang Liu, Jin Song Dong and Xian Zhang. ''[[Verifying Stateful Timed CSP using Implicit Clocks and Zone Abstraction|http://www.springerlink.com/content/t5120281288446k2/]]''. 11th International Conference on Formal Engineering Methods (ICFEM 2009). pages 581-600, Rio de Janeiro, Brazil, December, 2009. ([[Pdf|publications/ICFEM09a.pdf]], [[Bib|publications/bibs.html#icfem09a]], [[Slides|publications/PAT-Presentation-ICFEM2009a.pptx]])
# Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu and Jin Song Dong. ''[[Fair Model Checking with Process Counter Abstraction|http://www.springerlink.com/content/g9x418h563240884/]]''. The 16th International Symposium on Formal Methods (FM 2009). pages 123 - 139, Eindhoven, the Netherlands, November, 2009. ([[Pdf|publications/fm09Counter.pdf]], [[Bib|publications/bibs.html#fm09b]], [[Slides|publications/fm09Counter.zip]])
# Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. ''[[Model Checking Lineariability via Refinement|http://www.springerlink.com/content/5l72546040254p24/]]''. The 16th International Symposium on Formal Methods (FM 2009). pages 321-337, Eindhoven, the Netherlands, November, 2009. ([[Pdf|publications/linearizability.pdf]], [[Bib|publications/bibs.html#fm09a]], [[Slides|publications/linearizability.ppt]])
# Jun Sun, Yang Liu, Jin Song Dong and Jun Pang. ''[[PAT: Towards Flexible Verification under Fairness|http://www.springerlink.com/content/0321170v636j1853/]]''. The 21th International Conference on Computer Aided Verification (CAV 2009), pages 709-714, Grenoble, France, June, 2009. ([[Pdf|publications/cav09.pdf]], [[Bib|publications/bibs.html#cav09]], [[Slides|publications/cav-slides.ppt]]).
# Jin Song Dong and Jun Sun. ''[[Towards Expressive Specification and Efficient Model Checking|http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5198481]]'' (invited tutorial). The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), page 9, Tian Jing, China, July, 2009. ([[Pdf|publications/tase09invited.pdf]], [[Bib|publications/bibs.html#tase09a]], [[Slides|publications/taseTutorial.zip]]).
# Yang Liu, Jun Pang, Jun Sun and Jianhua Zhao. ''[[Verification of Population Ring Protocols in PAT|http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5198490]]''. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pages 81 - 89, Tian Jing, China, July, 2009. ([[Pdf|publications/tase09b.pdf]], [[Bib|publications/bibs.html#tase09b]], [[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://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=5198495]]''. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pages 127 - 135, Tian Jing, China, July, 2009. ([[Pdf|publications/tase09.pdf]], [[Bib|publications/bibs.html#tase09c]], [[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''. The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE 2009), pages 406-411, Boston, Massachusetts, USA, July 1-3, 2009. ([[Pdf|publications/seke09.pdf]], [[Bib|publications/bibs.html#seke09]], [[Slides|publications/seke09.ppt]]). //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.springerlink.com/content/y436513803766164/]]''. The 10th International Conference on Formal Engineering Methods (ICFEM 2008), pages 318-337, Japan, October, 2008. ([[Pdf|publications/icfem2008.pdf]], [[Bib|publications/bibs.html#icfem08b]], [[Slides|publications/icfem08.ppt]]). //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.//
# Jun Sun, Yang Liu and Jin Song Dong. ''[[Model Checking CSP Revisited: Introducing a Process Analysis Toolkit|http://www.springerlink.com/content/p0v16j3660211015/]]''. The Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008), pages 307-322, Porto Sani, Greece, October 13-15, 2008. ([[Pdf|publications/ISoLA08.pdf]], [[Bib|publications/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://portal.acm.org/citation.cfm?id=1382381]]''. The 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), pages 23-30, Nanjing, China, June 17-19, 2008. ([[Pdf|publications/TASE2008.pdf]], [[Bib|publications/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://portal.acm.org/citation.cfm?doid=1370175.1370187]]''. ICSE Companion, pages 919-920, Leipzig, Germany, 2008. ([[Pdf|publications/paticse08.pdf]], [[Bib|publications/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. //
<HTML>
In PAT, real-time systems are modeled using compositional timed processes. As to model the timed behaviors, instead of explicitly manipulating clocks, we dynamically create and prune clocks by implementing a number of timed behavior patterns such as delay, timeout, deadline, waituntil, timed interrupt, within, etc.
<br>The following experiments shows 5 popular real time system models which is used by lots of model checkers such as KRONOS and UPPAAL. In the experiments, we reasoned about various behaviors about the real time systems such as deadlock freeness, mutual exlucsion, liveness and safety properties. Details are elaborated as follows:
<br></br>—Fischer’s mutual exclusion protocol: The protocol is proposed by Fischer in 1985. Instead of using atomic test-and-set instructions or semaphores, mutual exclusion is guaranteed by carefully placing bounds on the execution time of the instructions, leading to a protocol which is simple and relies heavily on time aspects. The property is mutual exclusion.
<br>—Railway control system: A railway control system controls trains passing a critical point such as a bridge. The idea is to use a computer to guide trains from several tracks crossing a single bridge instead of building many bridges. Obviously, a property of such a system is that a train always eventually passes the bridge.
<br>—CSMA/CD protocol: This protocol describes a solution to the problem of assigning the bus to only one of many competing stations arises in a broadcast network with a multi-access bus. The property is that a collision is always eventually detected. The model is based on the one in KRONOS [BDM+98], extended to arbitrary number of stations.
<br>—Fiber Distributed Data Interface (FDDI): FDDI is a high-performance fiber-optic token ring local area network. An FDDI network is composed by N identical stations and a ring, where the stations can communicate by synchronous messages with high priority or asynchronous messages with low priority. The property is that the token cannot be in two stations simultaneously which is the safety property.
<br>— Timed Pacemaker: Pacemaker is a small device placed in the chest or abdomen to help control abnormal heart rhythms. It’s critical real time application that with a complex hierarchical structure that is deemed to be too complicated to be modeled in Timed Automata, while it is feasible for PAT to model it. A simple property is that the pacemaker is deadlock-free.
</br>
<br>Experiment results are shown in the table below. Here Time_zeno means that the property is verified with non-Zenoness check. We also done the comparison work with UPPAAL, and here UPPAAL-r means a revised version of its original models with some τ -transitions to make them consistent with our PAT model.
</br>
<CENTER>
<IMG WIDTH=880 SRC="./experiments/RTS.PNG" BORDER="0" ALT="">
</CENTER>
<br>From the experiments, we can see that PAT Real Time System Module can handle a rich set of properties within reasonable time. Also, a number of observations are here: Firstly, PAT currently handles in average 13, 000 states per second (i.e., the total number of visited states - not new states - divided by the total number of seconds), which is comparable to existing model checkers. Secondly, model checking with non-Zenoness has little or no computational overhead in PAT. Thirdly, PAT is considerably slower than UPPAAL. A number of reasons might account for why UPPAAL outperforms PAT. For instance, system configurations in PAT are more complicated than those in UPPAAL as Stateful Timed CSP is designed for hierarchical complex systems. The main reason is that UPPAAL has benefited from many dedicated optimization techniques such as extrapolation, however PAT has none yet. The experiment data is available <A href="./experiments/RTS.zip">here</A>.</br>
</HTML>
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. ''
!''Applying Model Checking to different domains''
* Modeling and verification of security procotol (in design phase)
* Modeling and verification of Orc language (in optimization)
* Modeling and verification of BPEL language (in implementation)
* Modeling and verification of Sensor networks system written in NesC (in optimization)
* Modeling and verification of Context-aware systems (in design phase)
* Verification of UML (or FUML) diagram (in design phase)
* Verification of Software Architecture Description Language (in implementation)
* Verification of System of Systems: Event Grammar (in implementation)
* Verification of C# Programs (in progress)
* Assembly Code Verification (in implementation)
!''Mode Checking Techniques Development''
* Automatic symmetry detection and reduction; We are looking for ways of applying symmetry reduction techniques to general systems without much changing of the modeling language. (in design phase).
* Stochastic Model Checking (in implementation)
* Symbolic modeling checking library (using BDD) for hierarchical systems (in testing phase)
* Assume-guarrantee verification (in implementation)
* Multi-core model checking algorithms and swarm verification techiniques (in implementation)
!''Others''
* Code generation from PAT models to C/C++ code for embedded system or mobile applications (in design phase)
* UTP language semantics of the PAT modeling languages (in progress)
* Visual Studio/Eclipse integration of PAT to allow users to link the source code with PAT for the direct verification of source code level. (in design phase)
* 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 deployment phase).
* Systematic comparision of PAT with other model checkers like FDR/SPIN/Uppaal/PRISM/NuSMV
!''Finished Features''
* BDD verification engine for CSP module is implemented (Version 3.4.1)
* Translation from Promela to CSP#
* Translation from Statechart to CSP#
* Find Usage and Renaming functions are supported in Editor(Version 3.2.2)
* Module Generator (Version 3.2.2)
* Model Explorer in the GUI (Version 3.2.1)
* Graphic User Interface for Drawing Processes
* [[1, Aug, 2010: PAT 3.1.0 is released. PAT is cross-platform now: running on Linux, Mac OS and more!]] (Version 3.1.0)
* System redesign with new text editor (Version 3.0.0)
* PRTS Module (Version 3.0.0)
* Safety properties detection and verification (Version 2.8.0)
* Refactoring Functions for the model editing: Goto Definition (for variable or process), Rename (variable and processes) (Version 2.7.0).
* [[25, Sep, 2009: PAT supports user defined data structures]] (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. Three 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 allmodules.
!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]].
* PAT is formally verified by [[Contracts|http://research.microsoft.com/en-us/projects/contracts/]] and [[Spec#|http://research.microsoft.com/en-us/projects/specsharp/]].
!Screen Shots
Screen Shots of PAT version 2.2.0 is avaiable [[HERE|Screen Shots]].
<HTML>
TA module in PAT is designed to verify systems which can be modeled as
networks of timed automata extended with shared variables, structured data types, user defined functions, and channel synchronization.
The following demonstrates the experimental results on embedded examples
in TA module and UPPAAL as well as the explanations of experiment
results.
<br></br>
We run experiments on four models, namely, Fischer protocol, railway
control systems, FDDI protocol and CSMACD protocol to verify properties
such as deadlock-freeness, liveness, reachability and so on. The
following table summarizes the verification results. Here, 'Proc' means
the number of interleaving processesand '-' means out of memory or more
than 2 hours. We also do the comparison work with UPPAAL, and here 'UPPAAL-r' means a recvised version of the original models in UPPAAL to make them consisten with the models in PAT, 'State-s' means the bumber of stored states,
'State-e' means the number of explored states. The environment of experiments ruuning on UPPALL 4.1.2 is as follows:
<ol>
<li>Use convex-hull approximation</li>
<li>Hash table size 16M</li>
<li>Automatic extrapolation operator</li>
<li>Depth First Search</li>
<li>Conservative space consumption</li>
<li>Enable sweepline method</li>
<li>Enable peephole optimiser</li>
<li>Enable symmetry reduction</li>
<CENTER>
<IMG WIDTH=800 SRC="./experiments/TA.PNG" BORDER="0" ALT="">
</CENTER>
From the above table, we can see that PAT TA module can verify a rich set of priorities with reasonable time. In addition, some abservations are here:
firstly, we can see that the number of states and
running time increase rapidly with increasing the number of processes,
e.g., 8 processes in Fischer model vs. 9 processes. Secondly, PAT is
efficient and can handle million states in less than one hour. Thirdly,
in some case, PAT is slower than UPPAAL. The main reason of UPPAAL outperforming
PAT is that UPPAAL has benefied from many dedicated optimization techniques such
as extrapolation, while PAT has none yet. The experiment data is available <a href="./experiments/TA.zip">here</a>.
</HTML>
!User Manual
The user manual is available ''[[online|OnlineHelp/index.htm]]''.
The CHM version can be downloaded ''[[HERE|OnlineHelp/Help.zip]]''.
The PDF version can be downloaded ''[[HERE|OnlineHelp/Help.pdf]]''.
If you are interested in the technical details of PAT, refer to our [[Publications]].
!API for PAT.Common.dll
The CHM version can be downloaded ''[[HERE|OnlineHelp/API.zip]]''.
This file include all methods and fields for PAT.Common project. All module needs to follow these APIs in order to be recongnized by PAT framework.
Please refer to user manual on how to use the APIs to develop custimized module in PAT.
!Documantation and Tutorials of PAT
1 [[PAT Getting Started-1|start.zip]] [[PAT Getting Started-2|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 3.5.0 Build 21221''
[[28, Dec, 2012: PAT 3.5.0 is released!]]
!''Version 3.4.4 Build 20502''
[[30, July, 2012: PAT 3.4.4 is released!]]
!''Version 3.4.3 Build 20099''
[[15, April, 2012: PAT 3.4.3 is released!]]
!''Version 3.4.2 Build 19913''
7, March, 2012
1 Bug fixing for RTS module, particularly for the atomic keyword.
2 For RTS module, global variables are disabled in timed processed.
3 All BEEM examples are added in for PAT.
4 Bug fix in using constants in LTL properties.
!''Version 3.4.2 Build 19689''
[[4, Feb, 2012: PAT 3.4.2 is released!]]
!''Version 3.4.1 Build 19499''
19, Jan, 2012
1 in CSP module, macro support if and while in the declaration.
2 Better self-composition detection is implemented in CSP module to avoid crash of PAT
3 More BEEM exampels are added (work in progress)
4 Invalided statement checking is added in all modules.
5 Flashing in the model checking window when the verification is finished.
6 Auto-update is avaiable for this release.
!''Version 3.4.1 Build 19462''
14, Jan, 2012
1 in CSP module, channels can attach programs
For the synchronous and asynchronous channel,
channel c 0; or channel c 1;
var x = 1;
P = c!x{ x = 2 } -> P;
Q = c?y{ x = y; } -> Q;
A = P ||| Q;
The execution sequence is c!x -> (x = 2) -> c?y -> (x = y)
2 Bugs fixing in CSP module and RTS module
3 More BEEM exampels are added (work in progress)
!''Version 3.4.1 Build 19371''
5, Jan, 2012
1 Code generation is supported for CSP module (beta version, based on QP platform)
2 BDD support for CSP module is done
3 Bitwise operator for integers is supported in all basic 5 modules: & (and), | (or) and xor (^)
4 Some BEEM database examples are added (work in progress)
5 RTS module parser update to support channel array and process parameter range
6 Parser bug fixing and macro is supported in all basic 5 modules
7 RTS non-zeno checking with zone abstraction performance improvement
!''Version 3.4.1 (Beta) Build 19079''
7, Dec, 2011
1 Fix the semantics of interrupt
2 Disable the support for BDD if there is a hiding in the process.
3 Support Macro in the CSP and RTS module.
''#define multi(i,j) i*j;''
''System = if (call(multi, 3,4) >12 ) { a -> Skip } else { b -> Skip }; ''
This could be useful to define some functions then you can use the function directly in the model.
Before you have to use C# static method to do this, now PAT offers another choices.
!''Version 3.4.1 (Beta) Build 19066''
23, Nov, 2011
1 Performance improvement for BDD verification of CSP module
2 RTS module bug fixing and simulation display improvement
3 Bug fixed for the array index assignment in all modules
4 Verification result with improved coloring
5 Add exception stack display in the method call exception.
6 Statistic display improvement for all modules in verification window.
!''Version 3.4.1 (Beta) Build 18833''
15, Nov, 2011
1 BDD support for CSP module is ready for testing. Wild Variable is also supported.
2 RTS module supports guard and ifa now. Parsing will fail if timed process is immediately following the guard and ifa.
e.g., P = [cond](Wait[5]);
3 A number of bug fixing for parsers in all modules.
4 Skip checking inside sequential composition is added and improved for all modules.
5 using direct array in process arguments and call arguments are supported.
e.g.
var <IntArrayList> intList;
intList.Add([1, 2, 3, 4, 5]);
6 font fixing for 64bit Windows machine.
!''Version 3.4.0 Build 18776''
06, Nov, 2011
1 xor operator is supported in CSP/RTS/PCSP module.
2 Generate witness trace check box is supported in verification window. you can uncheck it if the counterexample takes too long to generate or not important.
3 LTL parser bug is fixed
4 Bugs fixing in call method
5 Auto update is released.
!''Version 3.4.0 Build 18671''
20, Oct, 2011
1 Select is supported in LTS
2 Global variable update fixing in all modules.
3 Bug fixing in PCASE in PCSP module.
4 Auto update is released.
!''Version 3.4.0 Build 18653''
18, Oct, 2011
1 Bug fixing for variable range checking.
2 Bug fixing for RTS module, particularly digitalization.
3 Auto update is released for Version 3.4.0
!''Version 3.4.0 Build 18600''
5, Oct, 2011
1 Bug fixing for parallel compositional pattern.
2 Some examples update for CSP module.
!''Version 3.4.0 Build 18595''
2, Oct, 2011
1 Cancel and excepiton during the verification will give more infomation now
2 Parser for all modules are updated for the case that user defined data structure is used in the process parameters.
3 TA module updated with BDD support, also automata local variables are supported.
4 Self-looping process is detected in parser to avoid PAT easy crash
5 New BFS search engine is added for reachablity checking with min/max conditions (Beta).
6 Compositional detection of Skip in the sequential composition. Previously, P = (Skip ||| Skip); a -> Skip; has 3 states. Now it has only 2 states.
7 BDD for CSP module is disabled since it is not stable at the moment.
!''Version 3.4.0 Build 18409''
31, Aug, 2011
1 PAT now supports channel arrays, which is a syntax suger to make the modeling easier if the channels are parameterized. The following syntax demonstrates how to use the channel array.
channel c[3] 1;
Sender(i) = c[i]!i -> Sender(i);
Receiver() = c[0]?x -> a.x -> Receiver() [] c[1]?x -> a.x -> Receiver() [] c[2]?x -> a.x -> Receiver();
System() = (||| i:{0..2}@Sender(0) ) ||| Receiver();
Note: Two or N dimentional channel array can be simulated by using 1 dimentional channel array. Hence, we don't provide syntax support for that. For example channel c[3][5] 1 is same as channel c[15] 1, and c[2][3]!4 -> Skip is same as c[2*N+3]!4 -> Skip, where N is the first dimention.
2 3. CSP Module supports symbolic model checking using BDD (Beta version, under testing and optimization)
!''Version 3.4.0 Build 18350''
[[28, Aug, 2011: PAT 3.4 (beta) is released!]]
!''Version 3.3.1 Build 17101''
[[27, April, 2011: PAT 3.3.1 is released!]]
!''Version 3.3.0 Build 16884''
2, April, 2011
1 File Inclusion is improved to allow nested inclusion.
User can split the big models in several files for better orginization.
Find Usage, Go to declarision, and model explorer is improved to support multiple files.
2 Auto-updating checking is improved by a separate thread in the backend.
3 Calling C code is possible in PAT with one demonstrating example
4 GUI bug fixing.
!''Version 3.3.0 Build 16818''
1 Include keyword is added in CSP, PCSP, RTS and PRTS module to include other models in the current working model.
2 GUI bug fixing and enhancemant.
3 Auto-updating form is blocked by the splash screen
!''Version 3.3.0 Build 16750''
[[18, March, 2011: PAT 3.3.0 is released!]]
!''Version 3.2.3 Build 16562''
[[28, Feb, 2011: PAT 3.2.3 is released!]]
!''Version 3.2.2 Build 16422''
30, Jan, 2011
1 Renaming Functions is supported in the Editor
2 Module Generator is improved with better GUI, complete generated code. Module icon is also supportted in the
generated code.
3 Minor Bugs in the GUI are fixed.
!''Version 3.2.2 Build 16302''
[[21, Jan, 2011: PAT 3.2.2 is released!]]
!''Version 3.2.1 Build 16181''
26, Dec, 2010
1 Bugs for alphabet calculation are fixed in all modules.
2 Model Explorer is added in the GUI.
3 More examples are added in the CSP module.
!''Version 3.2.0 Build 16032''
8, Dec, 2010
1 Intellesense bug is fixed.
2 Bugs in PCSP module is fixed.
3 Precision in PCSP module is changed from float to double, so that we can handle precision at level of 10^-15.
4 BDD is working in 64 Bit now.
When you update the old version of 64 bit to new version using auto-update, please replace the CUDDHelper.dll
in the installation folder using the one under 64Bit folder. Otherwise the BDD funtion will not work correctly.
!''Version 3.2.0 Build 16003''
3, Dec, 2010
1 Bug in PCSP is fixed.
2 Auto-update is ready for the new version.
!''Version 3.2.0 Build 15997''
26, Nov, 2010
1. Some parsing errors are fixed.
e.g. P = e{;} ->Skip;
2. Intelli-sense is disabled when in comment
3. DLLs can be put under the same folder as in Model.
4. Other bug fixing.
5. Manual update
!''Version 3.2.0 Build 15962''
23, Nov, 2010
1 Mono execution is fixed in Mac and Linux.
2 LTL verification algorithms are reimplemented.
3 Bugs in RTS timed divergence checking are fixed.
4 Arrays are supported in local variables.
5 MDP verification are speed up (experimenting)
!''Version 3.2.0 Beta Build 15605''
22, Oct, 2010
1 Bug fixing on GUI and Mono execution.
2 Language localization for Chinese, Traditional Chinese and Vietnamese are improved.
!''Version 3.2.0 Beta Build 15506''
6, Oct, 2010
1 Bug fixing for all modules
2 TA module supports select syntax, examples are added
3 Refinement checking's performance is improved significantly
4 LTS module is re-structured
5 RTS module's performance is improved by using maximun delay after one step.
!''Version 3.2.0 Beta Build 15288''
2, Sep, 2010
[[2, Sep, 2010: PAT 3.2.0 (beta) is released!]]
!''Version 3.1.0 Build 146599''
1, Aug, 2010
[[1, Aug, 2010: PAT 3.1.0 is released. PAT is cross-platform now: running on Linux, Mac OS and more!]]
!''Version 3.0.0 Build 14419''
19, July, 2010
1 Bug fixed in the auto-updating file
2 Directory mode is added in PAT.Console. User can put all models into a directory and use console to run all all of them.
!''Version 3.0.0 Build 14399''
15, July, 2010
[[14, July, 2010: PAT 3.0.0 is released!]]
!''Version 3.0.0 Build 14150''
1, June, 2010
Fix the bug for auto updating, please reinstall PAT 3.0 in order to make auto update working.
!''Version 3.0.0 Build 14116''
30, May, 2010
Bug fixing, mainly for RTS module
!''Version 3.0.0 Build 14000''
22, May, 2010
[[22, May, 2010: PAT 3.0.0 beta is released!]]
!''Version 2.9.1 Build 12592''
18, March, 2010
[[18, March, 2010: PAT 2.9.1 is released!]]
!''Version 2.9.0 Build 12592''
23, Feb, 2010
1 Bug fixing for refinement checking with failures and divergence.
2 User manual is updated.
!''Version 2.9.0 Build 12511''
10, Feb, 2010
1 Bug fixing and improvement in all parsers.
2 Simulator is improved with complete state display
3 Images are added for sliding game and shunting game in the simulator (Contributed by Tian Huat)
4 User manuals are updated (by Liu Yan)
5 New example is added for DBM testing
!''Version 2.9.0 Build 12259''
4, Feb, 2010
1 Bugs fixed for parallel operator and refinement checking (for all modules)
2 Performance improved for refinement checking (10% - 15% speedup)
3 PAT.Math is supported for normal math functions
4 Duplicated edges are removed for hiding tau event in simulation
!''Version 2.9.0 Build 12259''
29, Jan, 2010
[[29, Jan, 2010: PAT 2.9.0 is released!]]
!''Version 2.8.0 Build 11674''
16, Dec, 2009
1 Several Bug logic and UI fix
2 Beta LTL to Rabin automata translator is implemented
3 Simplification for Skip and Stop in parallel/interleave/sequential processes.
!''Version 2.8.0 Build 11481''
05, Dec, 2009
1 Bug fix in verifier for reachability testing result display
!''Version 2.8.0 Build 11481''
04, Dec, 2009
1 Bug fix in parser
!''Version 2.8.0 Build 11465''
03, Dec, 2009
1 Bug fix in counter example display for safety property.
2 Shunting game example is added.
!''Version 2.8.0 Build 11450''
02, Dec, 2009
[[02, Dec, 2009: PAT 2.8.0 is released!]]
!''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.
We are making short videos for PAT basing modules. More videos are coming
PCSP Module: [[AVI Format|pcsp.avi]] [[youtube|http://www.youtube.com/watch?v=idk2MtW3Jnk]] Contributed by Song SongZheng
NESC Module: [[AVI Format|nesc.avi]] [[youtube|http://www.youtube.com/watch?list=UL&feature=mfu_in_order&hl=en&v=-bu_n64kGEA]] Contributed by Zheng ManChun
Originally, PAT supports only weak live and strong live events. To make PAT more useful, weak fair and strong fair events are supported.