Detection of Possible Frozen States in Communicating UML State Machines

One of the most important problems of verification of discrete event control systems is detection of possible incorrect communication between concurrent processes, such as mutual blocking. Processes can be modeled as state machines, and such detection can be performed by analysis of behavior of the communicating automata. For such analysis in general case the model checking methods are used, nevertheless some practically important results can be obtained by the methods with lower computational complexity. In the paper a special case of the problem is considered, which is a detection of possible frozen states in a pair of communicating state machines. The algorithm solving this task is presented, its computational complexity is evaluated.