PAT: Process Analysis Toolkit

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

Monthly archives for July, 2008

31, July, 2008: PAT 1.2.2 is released!

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.
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.

10, July, 2008: PAT 1.2.0 is released!

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.”

Process level fairness is supported: include global, strong and weak fairness

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.