Model checking of control-finite CSP programs

The authors investigate an automatic verification mechanism for control-finite communicating sequential processes (CSP) programs by using the model checking technique. CSP programs with variables and usual sequential constructs are transformed into transition systems to apply the model checking technique. More specifically, binding of variables are attached to states and sequential statements are treated uniformly as events in a parallel environment. With this transformation, the system can be viewed as implementing the model checker for a static version of value-passing CCS. Another characteristic of the system is that the CSP programs to be verified are not limited to finite-state, but can be control-finite, CSP programs are control-finite if their control flow is finite. The model checker was implemented and various examples of parallel programming were verified