Deadlock detection in distributed systems using the IMDS formalism and Petri nets

Daszczuk, W.B., Zuberek, W.M.

in: Advances in Dependability Engineering of Complex Systems (Advances in Intelligent Systems and Computing 582), Proc. of the 12-th Int. Conf. on Dependability and Complex Systems (DepCoS-RELCOMEX'17), 3 - 6 July 2017, Brunow Palace, Poland, ed. Zamojski W., Mazurkiewicz J., Sugier J., Walkowiak T., Kacprzyk J., pp.118-130, Springer-Verlag 2017 (DOI 10.1007/978-3-319-59415-6).


Integrated Model of Distributed Systems (IMDS) is a formalism which expresses duality of message passing and resource sharing and which highlights locality, autonomy of distributed elements as well as asynchrony of actions and communication. Combined with model checking, IMDS allows to verify numerous properties of modeled systems. It also provides insights into the behavior of model components (servers and agents) in the form of server view and agent view of the system. IMDS is used in the Dedan verification environment which can detect several types of deadlocks, including communication deadlocks (in the server view) and resource deadlocks (in the agent view). The paper also outlines a mapping of IMDS models into behaviorally equivalent Petri nets, opening the way for many analysis techniques developed for Petri nets to be used for analysis of IMDS models. In particular, structural (siphon-based) methods for deadlock analysis in Petri nets can be used for deadlock detection in IMDS models.



distributed systems, distributed system modeling, deadlock detection, Petri nets, Petri net siphons

Available in pdf.