In this paper we are interested in the verification of saftey properties of parameterized networks. A network is defined as a parallel copmosition of an arbitrary but finite number of identical sequential processes, where we consider parallel composition by interleaving and synchronization by shared variables. Using abstraction techniques, a process, called an abstract network, encoding the entire network is constructed. the property is then checked on this process. Our verification method has the following advantages: the construction of the abstract network id fully automatic; the obtained process is generally a simple process on which the property can be easily verified. Of course, if the property cannot be verified on the abstract network, another more precise abstraction has to be computed. The construction requires to discharge a set of first order verification conditions (VCs). The PVS theorem prover is used to discharge the generated VCs. This allows us to consider processes with arbitrary data types. The effectivness of our verification method is illustrated on two examples including a parametreized version of the Fischer's protocol.

• LesensSaidi97.ps.gz