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 12th Int. Conf. on
Dependability and Complex Systems (DepCoSRELCOMEX'17), 3  6 July 2017,
Brunow Palace, Poland, ed. Zamojski W., Mazurkiewicz J., Sugier J.,
Walkowiak T., Kacprzyk J., pp.118130, SpringerVerlag 2017
(DOI 10.1007/9783319594156).
Abstract:
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 (siphonbased)
methods for deadlock analysis in Petri nets can be used for deadlock detection
in IMDS models.
References:

Chrobot, S., Daszczuk, W.B., ``Communication dualism in distributed systems
with Petri net interpretation''; Theor. Appl. Informatics, vol.18, no.4,
pp.261278, 2006.

Daszczuk, W.B., ``Deadlock and termination detection using IMDS formalism
and model checking; version 2''; ICS WUT Technical Report no.3/2008, 2008.

Daszczuk, W.B., ``Communication and resource deadlock analysis using IMDS
formalism and model checking''; The Computer Journal (in print).

Clarke, E.M., Grumberg, O, Peled, D., Model checking, MIT Press 1999
(ISBN 0262032708).

Dedan, http://staff.ii.pw.edu/dedan/files/DedAn.zip.

Reisig, W., Petri nets ‐ an introduction; SpringerVerlag 1985
(ISBN 9783642699702).

Boer, E.R., Murata, T., ``Generating basic siphons and traps of Petri nets
using the sign incidence matrix''; IEEE Trans. on Circuits and Systems I:
Fundam. Theory Appl., vol.4, no.4, pp.266271, 1994.

Chu, F., Xie, XL., ``Deadlock analysis of Petri nets using siphons and
nathematical programming''; IEEE Trans. on Robotics and Automation, vol.13,
no.6, pp.793804, 1997.

Reniers, M.A, Willemse, T.A.C., ``Folk theorems on the correspondence between
statebased and eveentbased systems''; Proc. 37th Conf. on Current Trends in
Theory and Practice of Computer Sicence, Novy Smokovec, Slovakia, pp.494505,
2011.

Penczek, W., Szreter, M., Gerth, R., Kuiper, R., ``Improving partial order
eductions for universal branching time properties''; Fundamenta Informaticae,
vol.43, no.14, pp.245267, 2000.

Czejdo, B., Bhattacharya, S., Baszun, M., Daszczuk, W.B., ``Improving
resilience of autonomousmoving platforms by realtime analysis of their
cooperation''; AutobusyTEST, vol.17, no.6, pp.12941301, 2016.

Charlie: Charlie Petri net analyzer;
http://wwwdssz.informatik.tucottbus.de/DSSZ/Software/Cherlie.

Heiner, M., Schwarick, M., Wegener, JT., ``Charlie  and extensible Petri net
analysis tool''; Proc. 36th Conf. on Application and Theory of Petri Net,
Brussels, Belgium, pp.200211, 2015.

Schwarick, M., Heiner, M., Rohr, C., ``MARCIE  model checking and reachability
analysis done efficiently''; Proc. 8th Int. Conf. on Quantitative Evaluation
of Systems, Aachen, Germany, pp.91100, 2011.

Behrman, G., David, A., Larsen, K.G., ``A tutorial on UPPAL 4.0''; Report
Univ. Aalborg, Denmark 2006.
Keywords:
distributed systems, distributed system modeling, deadlock detection,
Petri nets, Petri net siphons
Available in pdf.