Automatic Verification of Parameterized Networks of Processes
Abstract:
This paper describes a method to verify safety properties of
parameterized networks of processes defined by network grammars.
The method is based on the construction of a network invariant,
defined as a fixpoint. We propose heuristics, based
on Cousot's extrapolation techniques (widening), which often allow
suitable invariants to be automatically constructed.
We successively consider linear and binary tree networks.
These techniques have been implemented in a verification tool, and
several non-trivial examples are presented.
Reference:
@article{
author={D. Lesens and N. Halbwachs and P. Raymond},
title={Automatic Verification of Parameterized Networks of Processes},
journal={Theoretical Computer Science},
volume = {256},
year=2001,
pages={113--144}
}