PAT: Process Analysis Toolkit

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

Monthly archives for May, 2008

25, May, 2008: PAT is presented in ICSE 2008

PAT is presented in ICSE 2008.

The presentation poster is here:
PAT Poster


Clicking on links to tiddlers that are already open causes them to close
(override with Control or other modifier key)
HideEditingFeatures when viewed over HTTP
Treat edits as MinorChanges by preserving date and time
(override with Shift key when clicking ‘done’ or by pressing Ctrl-Shift-Enter
Maximum number of lines in a tiddler edit box:
Folder name for backup files:
Use tab key to insert tab characters instead of jumping to next field

5, May, 2008: PAT wants You!

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.

Complete the unit testing

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 as the unit testing tool. Hopefully, we can complete the unit testing to catch up the latest development.

Simulation window is redesigned completely

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.

5, May, 2008: The PAT’s User Interface and Language Parser are completely redesigned.

For the details, check it out:
Post to Post Links II error: No post found with slug "add-the-syntax-checking-after-parsing-to-rule-out-invalid-un-declared-variables-usage"
Simulation window is redesigned completely

Weak Fair and Strong Fair annotations are supported by PAT now

Originally, PAT supports only weak live and strong live events. To make PAT more useful, weak fair and strong fair events are supported.

Add the syntax checking after parsing to rule out invalid/un-declared variables usage

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.