Language-based analysis of communicating finite state machines.

Abstract

Protocol validation has traditionally focused on detecting errors defined in terms of global states. A complementary approach is to analyze the process languages of a protocol, where a process language is defined as the set of executable event sequences of a process in the protocol. A general property of a process is "effectiveness", defined as the absence of unexecutable specified event sequences. A method is given for determining whether a specified process (the "host process") in a protocol is effective. The method involves generating a process language's finite state machine representation, called a process event graph (PEG). Every PEG node maps to a global state. Using the given method to generate a PEG, it is shown that, when the PEG generation does not detect error states, every reachable global state is reachable from a PEG node by an event sequence that does not include any host events. This introduces the possibility of a parallel approach to reachability analysis, in which a PEG is generated, and then a "local" reachability analysis is performed from each PEG node in parallel, ignoring host events. Other applications of PEGs are also given.