Download Latest Version

PaMC is a model checker specialised for verifying safety properties of parameterized systems which consists of an indefinite number of identical processes running in parallel. It implements a very powerful abstraction technique known as parameter abstraction and guard strengthening, using a heuristics-based automatic procedure to compute auxiliary invariants. Experiments show that PaMC is powerful enough to verify complex real-life parameterized systems such as Godson-T cache coherence protocol.

Overview

PaMC is a model checker designed for verifying safety properties of parameterized systems. A parameterized systems P(N), where N is the parameter of the system, consists of N identical processes running in parallel. Example parameterized systems include many network protocols and cache coherence protocols. Although the model checking problem for such systems is undecidable in general, many abstraction techniques have been proposed for various subclasses of parameterized systems which work well in practice. PaMC is based on a very powerful abstraction technique known as parameter abstraction and guard strengthening.


PaMC is written in C. Its syntax parser and BDD library operation procedure are adapted from TLV. PaMC implements the parameter abstraction, invariants computing and guard strengthening procedure. However, we do not try to make PaMC a stand-alone model checker. Instead, it can use any model checker which accepts SMV input language, such as TLV, Cadence SMV or NuSMV, as its model checking engine.

download

You can download the source and the binary of the latest version of PaMC PaMC-0.3.1-src.tgz and PaMC-0.3.1-bin.tgz. You can download the manual of PaMC here. Cubicle code for German-2004 and Godson-T can be downloaded here.

We suggest that the user installs Cadence SMV as the model checking engine of PaMC.

examples

Following shows a small example muxsem protocol of PaMC.

  •  1    --muxsem.pam--
  •  2    MODULE main
  •  3    VAR
  •  4      x : boolean;
  •  5      array Node[Proc] : node_module;
  •  6      array Request[Proc] : transition request(Node[Proc].State, x);
  •  7      array Enter[Proc] : transition enter(Node[Proc].State, x);
  •  8      array Release[Proc] : transition release(Node[Proc].State, x);
  •  9      array Idling[Proc] : transition idling(Node[Proc].State, x);
  • 10   ASSIGN
  • 11     init(x) := 1;
  • 12   SPEC
  • 13     FORALL(i,j)(i!=j -> !(Node[i].State = crit & Node[j].State = crit))
  • 14   MODULE node_module
  • 15   VAR
  • 16     State : {idle,try,crit,exiting};
  • 17   ASSIGN
  • 18     init(State) := idle;
  • 19   MODULE request(state, semaphore)
  • 20   ASSIGN
  • 21     next(state) := 
  • 22       case 
  • 23         state = idle : try;
  • 24         1 : state;
  • 25       esac;
  • 26   MODULE enter(state, semaphore)
  • 27   ASSIGN
  • 28     next(state) := 
  • 29       case 
  • 30         state = try & semaphore : crit;
  • 31         1 : state;
  • 32       esac;
  • 33     next(semaphore) := 
  • 34       case
  • 35         state = try & semaphore : 0;
  • 36         1 : semaphore;
  • 37       esac;
  • 38   MODULE release(state, semaphore)
  • 39   ASSIGN
  • 40     next(state) := 
  • 41       case 
  • 42         state = crit : exiting;
  • 43         1 : state;
  • 44       esac;
  • 45   MODULE idling(state, semaphore)
  • 46   ASSIGN
  • 47     next(state) := 
  • 48       case 
  • 49         state = exiting : idle;
  • 50         1 : state;
  • 51       esac;
  • 52     next(semaphore) := 
  • 53       case
  • 54         state = exiting : 1;
  • 55         1 : semaphore;
  • 56       esac;

contact

You can contact us at our respective email addresses.