Communication and Resource Deadlock Analysis Using IMDS Formalism and Model Checking

Modern static deadlock detection techniques deal with the global properties of the verified systems, using methods that explore the state space. Local features, like partial deadlocks or individual process terminations, are not easily expressed or checked by such methods. Also the distinction between communication deadlocks and resource deadlocks, common in dynamic waits-for methods, cannot be addressed or verified by static methods. An Integrated Model of Distributed Systems (IMDS) is proposed which specifies distributed systems as sets of servers' states, sets of messages and sets of actions. The message passing/resource sharing dualism of distributed systems is provided by projections: on servers (server view) and on agents (agent view), yet the uniform specification of a verified system is preserved. A progress of computation is defined in terms of actions which change (local) states and generate messages. Distributed actions do not depend on global states and are independent from one another. Therefore, local features of subsystems can be easily described in IMDS. Communication and resource deadlocks can be handled separately and total and partial deadlocks and terminations can be distinguished from each other. Integration of IMDS with model checking is outlined and temporal formulas for deadlock and termination checking are discussed.