Diagnostic tests for communicating finite state machines

The authors propose a diagnostic algorithm for the case where a protocol specification is given in the form of communicating finite state machines (CFSMs). Such an algorithm localizes the faulty transition in the protocol implementation once the fault has been detected. It generates, if necessary, additional diagnostic tests, which depend on the observed symptoms and which permit the location of the detected fault. The algorithm guarantees the correct diagnosis of any single fault in CFSMs. A simple example is used to demonstrate the different steps of the proposed diagnostic algorithm