Deadlock Detection in Distributed Systems Using the IMDS Formalism and Petri Nets

Wiktor B. Daszczuk , Włodzimierz M Zuberek

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 (siphon-based) methods for deadlock analysis in Petri nets can be used for deadlock detection in IMDS models.
Author Wiktor B. Daszczuk (FEIT / IN)
Wiktor B. Daszczuk,,
- The Institute of Computer Science
, Włodzimierz M Zuberek
Włodzimierz M Zuberek,,
-
Pages118-130
Publication size in sheets0.6
Book Zamojski Wojciech, Mazurkiewicz Jacek, Sugier Jarosław, Walkowiak Tomasz, Kacprzyk Janusz (eds.): Advances in Dependability Engineering of Complex Systems. Proceedings of the Twelfth International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, Advances in Intelligent Systems and Computing, vol. 582, 2018, Springer International Publishing, ISBN 978-3-319-59414-9, [978-3-319-59415-6], 488 p., DOI:10.1007/978-3-319-59415-6
Keywords in EnglishDistributed systems, Distributed system modeling, Deadlock detection, Petri nets, Petri net siphons, Formal methods 
DOIDOI:10.1007/978-3-319-59415-6_12
URL https://link.springer.com/chapter/10.1007/978-3-319-59415-6_12
projectDevelopment of new algorithms in the areas of software and computer architecture, artificial intelligence and information systems and computer graphics . Project leader: Arabas Jarosław, , Phone: +48 22 234 7432, start date 15-04-2016, end date 30-11-2017, II/2016/DS/1, Completed
WEiTI Działalność statutowa
Languageen angielski
File
PN_IMDS_5a.pdf 1.21 MB
Score (nominal)15
ScoreMinisterial score = 15.0, 21-06-2017, BookChapterSeriesAndMatConf
Ministerial score (2013-2016) = 15.0, 21-06-2017, BookChapterSeriesAndMatConf
Citation count*2 (2018-11-13)
Cite
Share Share

Get link to the record


* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Back