Deadlock Analysis in Statecharts.
Andrei G. Karatkevich · 2003
A method is proposed for detecting all reachable deadlocks in a discrete system specified by Statecharts. The detecting is performed by means of building and analyzing the reduced reachability graphs of the system or its parts. The method can be applied to formal verification of the concurrent logical control algorithms described in this language. 1