Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Advances in Dependability Engineering of Complex Systems (DepCoS-RELCOMEX 2017)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 582))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Chrobot, S., Daszczuk, W.B.: Communication dualism in distributed systems with Petri net interpretation. Theor. Appl. Inform. 18(4), 261–278 (2006)

    Google Scholar 

  2. Daszczuk, W.B.: Deadlock and termination detection using IMDS formalism and model checking, Version 2. ICS WUT Research Report No. 2/2008 (2008)

    Google Scholar 

  3. Daszczuk, W.B.: Communication and resource deadlock analysis using IMDS formalism and model checking. Comput. J. (2016) (in press). doi:10.1093/comjnl/bxw099

  4. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999). ISBN 0-262-03270-8

    Google Scholar 

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

  6. Reisig, W.: Petri Nets - An Introduction. Springer, Heidelberg (1985). ISBN 978-3-642-69970-2

    Book  MATH  Google Scholar 

  7. Craig, D.C., Zuberek, W.M.: Two-stage siphon-based deadlock detection in Petri nets. In: Petratos, P., Dandapami, P. (eds.) Current Advances in Computing, Engineering and Information Technology, pp. 317–330. International Society for Advanced Research, Palermo, Italy (2008). ISBN 978–960-6672-34-7

    Google Scholar 

  8. Chu, F., Xie, X.-L.: Deadlock analysis of Petri nets using siphons and mathematical programming. IEEE Trans. Robot. Autom. 13(6), 793–804 (1997). doi:10.1109/70.650158

    Article  Google Scholar 

  9. Reniers, M.A., Willemse, T.A.C.: Folk theorems on the correspondence between state-based and event-based systems. In: Černá I. et al. (ed.) 37th Conference on Current Trends in Theory and Practice of Computer Science, Nový Smokovec, Slovakia, 22–28 January 2011, pp. 494–505. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18381-2_41

  10. Penczek, W., Szreter, M., Gerth, R., Kuiper, R.: Improving partial order reductions for universal branching time properties. Fundam. Informaticae 43(1–6), 245–267 (2000). doi:10.3233/FI-2000-43123413

    MathSciNet  MATH  Google Scholar 

  11. Czejdo, B., Bhattacharya, S., Baszun, M., Daszczuk, W.B.: Improving resilience of autonomous moving platforms by real-time analysis of their cooperation. Autobusy-TEST 17(6), 1294–1301 (2016)

    Google Scholar 

  12. Charlie: Charlie Petri net analyzer. http://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Charlie

  13. Heiner, M., Schwarick, M., Wegener, J.-T.: Charlie – an extensible Petri net analysis tool. In: 36th International Conference, PETRI NETS 2015, Brussels, Belgium, 21–26 June 2015, pp. 200–211. Springer, Cham (2015). doi: 10.1007/978-3-319-19488-2_10

  14. Schwarick, M., Heiner, M., Rohr, C.: MARCIE - model checking and reachability analysis done efficiently. In: 2011 Eighth International Conference on Quantitative Evaluation of Systems, Aachen, Germany, 5–8 September 2011, pp. 91–100. IEEE, Los Angeles, CA (2011). doi:10.1109/QEST.2011.19

  15. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal 4.0. Report, University of Aalborg, Denmark (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Warsaw University of Technology, Nowowiejska Street 15/19, 00-665, Warsaw, Poland

    Wiktor B. Daszczuk

  2. Department of Computer Science, Memorial University, St. John’s, AlB 3X5, Canada

    Wlodek M. Zuberek

Authors
  1. Wiktor B. Daszczuk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wlodek M. Zuberek
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wiktor B. Daszczuk .

Editor information

Editors and Affiliations

  1. Department of Computer Engineering, Wrocław University of Technology Department of Computer Engineering, Wrocław, Poland

    Wojciech Zamojski

  2. Department of Computer Engineering, Wrocław University of Technology Department of Computer Engineering, Wrocław, Poland

    Jacek Mazurkiewicz

  3. Department of Computer Engineering, Wrocław University of Technology, Wroclaw, Poland

    Jarosław Sugier

  4. Department of Computer Engineering, Wrocław University of Technology Department of Computer Engineering, Wrocław, Poland

    Tomasz Walkowiak

  5. Systems Research Institute, Polish Academy of Sciences Systems Research Institute, Warsaw, Poland

    Janusz Kacprzyk

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Cite this paper

Daszczuk, W.B., Zuberek, W.M. (2018). Deadlock Detection in Distributed Systems Using the IMDS Formalism and Petri Nets. In: Zamojski, W., Mazurkiewicz, J., Sugier, J., Walkowiak, T., Kacprzyk, J. (eds) Advances in Dependability Engineering of Complex Systems. DepCoS-RELCOMEX 2017. Advances in Intelligent Systems and Computing, vol 582. Springer, Cham. https://doi.org/10.1007/978-3-319-59415-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-59415-6_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-59414-9

  • Online ISBN: 978-3-319-59415-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation