Automatic verification for a class of distributed systems

The paper presents a new analysis method for a class of concurrent systems which are formed of several interacting components with the same structure. The model for these systems is composed of a control process and a set of homogeneous user processes. The control and user processes are modeled by f inite labeled state transition systems which interact by means of enabling functions and triggering mechanisms. Based on this structure, an analysis m ethod is presented which allows system properties, derived by reachability analysis for a finite number of user processes, to be generalized to an arb itrary number of user processes. A procedure for the automatic Verification of properties such as mutual exclusion and absence of deadlocks is present ed and is then used to provide for the first time a fully automated verific ation of the Lamport's fast mutual exclusion algorithm.