UPPSALA UNIVERSITET : Institutionen för Informationsteknologi : Algorithmic Program Verification Group
Uppsala universitet

PFS webpage




Case Studies

Related Publications

PFS Prototype


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

parameterized system


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:
  1. A process can change the values of its local variables and possibly move to another control state.
  2. 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).
  3. 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).
Possible extensions consist in adding


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.


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.


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

Valid XHTML 1.0 Transitional Valid CSS!
Contact us
Noomene Ben Henda





Ahmed Rezine