PAT: Process Analysis Toolkit

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

02, Dec, 2009: PAT 2.8.0 is released!

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.

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.