PFS Prototype
Introdution
PFS is a prototype for the verification of parameterized systems. A parameterized system consists of an arbitrary number of identical state machines running in parallel. For instance, many cache coherence protocols as well as mutual exclusion algorithms fit into this modeling framework. The prototype performs backward reachability over an over-approximation of the system in order to check safety property. All details are in [1].
Models
The model we adopt is that of parameterized systems where each process is a finite-state machine; i.e., each process has a finite set of finite domain variables (including the control state). Transition within a process can be of one of the following forms:- A process can change the values of its local variables and possibly move to another control state.
- A process can chek if all other processes (or all processes to its left/right) satisfy a given condition over their local variables. In case yes, the process proceeds in a similar manner to rule (1).
- A process can chek if at least one other processe (or one process to its left/right) satisfies a given condition over its local variables. In case yes, the process proceeds in a similar manner to rule (1).
- finite domain shared (or global) variables which maybe changed during transitions like local variables (supported by the prototype);
- broadcast transition where a process (called initiator) forces all processes which satisfy a given condition to change states simultaneously, possibly their local variables too (supported by the prototype);
- dynamic creation and deletion of processes (supported by the prototype);
- binary communication where two processes change state simultaneously if they statisfy given conditions (not supported).
Properties
PFS checks parameterized system models against safety property. For instance, given a model (as described above), a configuration of the system is a sequence of process states, each describing the values of local variables and the current control state. If we assume that in the process model there is a critical control state, then the set of unsafe configuration correspond to the set of sequences containing at least two process states where the control location is critical. The goal is to check if the set of unsafe configurations is unreachable from the set of "initial" configurations regardless of the number of processes in the system.Download
PFS is free and open source. You can download the source code for free from below. Distribution is under the GNU General Public License (GPL). PFS runs on Linux. pfs.tar.gz.Instructions
After extracting the archive, read the file "README.txt". It should suffice to run "make depend" then "make main". The input language of the prototype is simple. Check the examples files to get inspired.Case studies
Follows some mutual exclusion algorithms and cache coherence protocols the safety of which was verifyed by PFS. Check the technical report for a detailed description.| Mutual Exclusion Algorithms | Iterations | Cache Coherence Protocols | Iterations |
|---|---|---|---|
| Bakery | 2 | Synapse | 3 |
| Bakery(*) | 2 | Berkley | 2 |
| Burns | 14 | Mesi | 3 |
| Burns(*) | 9 | Moeisi | 1 |
| Java M-lock | 5 | Dec Firefly | 3 |
| Java M-lock(*) | 5 | Xerox P.D | 3 |
| Dijkstra | 13 | Illinois | 5 |
| Dijkstra(*) | 8 | Futurebus | 7 |
| Szymanski | 17 | German | 44 |
| Szymanski(*) | 17 |
Here (*) means that processes may be non-deterministically created/deleted while in state "idle".
Besides the German protocol, the verification of which required 3h45mn, all these examples were verified in less than 5 seconds on a Pentium M 1.6 Ghz.
All case studies are fully described in [2].
Related Publications
[1] Main paper: Regular Model Checking without Transducers. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Proc. TACAS 2007, 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. PDF, PS.
[2] Technical report: Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems). Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. IT-database 2006. Link.
Presentation slides: tacas07-b4.pdf
. |
