Checking states and transitions of a set of communicating finite state machines

This paper considers the problem of testing to check the transitions of implementation I against those of a model M consisting of communicating finite state machines. One approach is to generate the product machine from M and then apply standard finite state machine test techniques. This approach may, however, suffer from a combinatorial explosion. Instead, this paper introduces approaches that may allow local states and transitions of I to be checked without the generation of the product machine. The paper then extends these approaches to the checking of global states