Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 15

Proceedings of the 2018 Federated Conference on Computer Science and Information Systems

Siphon-based deadlock detection in Integrated Model of Distributed Systems (IMDS)

DOI: http://dx.doi.org/10.15439/2018F114

Citation: Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 15, pages 425–435 ()

Full text

Abstract. Integrated Model of Distributed Systems (IMDS) is a formalism for specification and verification of distributed systems, especially following IoT (Internet of Things) paradigm. The formalism emphasizes such features as asynchrony of actions and communication, locality of decisions, and autonomy in executing actions. In conjunction with model checking, IMDS allows to analyze such features of distributed systems as deadlocks or distributed termination. However, the nature of model checking allows to find one deadlock in a single run of the verifier (a counterexample). The conversion of IMDS specification to a Petri net is used to identify multiple deadlocks in one verification, using siphons. Model checking is used to verify if a siphon can become empty. Siphon analysis is typically used to investigate deadlocks in purely cyclic FMS (Flexible Manufacturing Systems). The extension of the verification by temporal checking of deadlock occurrence allows to cover systems with any structure: cyclic, terminating, or with a more complex structure. In addition, IMDS allows to easily identify processes participating in partial deadlocks. Two types of deadlock can be identified: communication deadlocks and resource deadlocks.

References

  1. S. Chrobot and W. B. Daszczuk, “Communication Dualism in Distributed Systems with Petri Net Interpretation,” Theor. Appl. Informatics, vol. 18, no. 4, pp. 261–278, 2006. https://arxiv.org/abs/ 1710.07907
  2. W. B. Daszczuk, “Communication and Resource Deadlock Analysis using IMDS Formalism and Model Checking,” Comput. J., vol. 60, no. 5, pp. 729–750, 2017. http://dx.doi.org/10.1093/comjnl/bxw099
  3. C. Baier and J.-P. Katoen, Principles of Model Checking. Cambridge, MA: MIT Press, 2008. ISBN: 9780262026499
  4. Dedan, http://staff.ii.pw.edu.pl/dedan/files/DedAn.zip
  5. W. Reisig, Petri Nets - An Introduction. Berlin, Heidelberg: Springer Berlin Heidelberg, 1985. http://dx.doi.org/10.1007/978-3-642-69968-9
  6. D. C. Craig and W. M. Zuberek, “Two-stage siphon-based deadlock detection in Petri nets,” in Current Advances in Computing, Engineering and Information Technology, P. Petratos and P. Dandapami, Eds. Palermo, Italy: Int. Society for Advanced Research, 2008, pp. 317–330.
  7. F. Chu and X.-L. Xie, “Deadlock analysis of Petri nets using siphons and mathematical programming,” IEEE Trans. Robot. Autom., vol. 13, no. 6, pp. 793–804, 1997. http://dx.doi.org/10.1109/70.650158
  8. M. Uzam, “An Optimal Deadlock Prevention Policy for Flexible Manufacturing Systems Using Petri Net Models with Resources and the Theory of Regions,” Int. J. Adv. Manuf. Technol., vol. 19, no. 3, pp. 192–208, Feb. 2002. http://dx.doi.org/10.1007/s001700200014
  9. J. Ezpeleta, J. M. Colom, and J. Martinez, “A Petri net based deadlock prevention policy for flexible manufacturing systems,” IEEE Trans. Robot. Autom., vol. 11, no. 2, pp. 173–184, Apr. 1995. http://dx.doi.org/10.1109/70.370500
  10. W. B. Daszczuk and W. M. Zuberek, “Deadlock Detection in Distributed Systems Using the IMDS Formalism and Petri Nets,” in 12th International Conference on Dependability and Complex Systems, DepCoS-RELCOMEX 2017, Brunów, Poland, 2-6 July 2017. AISC vol 582, W. Zamojski et al., Eds, Cham, Switzerland: Springer International Publishing, 2018, pp. 118–130. http://dx.doi.org/10.1007/978-3-319-59415-6_12
  11. R. Agarwal and S. D. Stoller, “Run-Time Detection of Potential Deadlocks for Programs with Locks, Semaphores, and Condition Variables,” in Proc. of the Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD-IV), ISSTA, 2006, Portland, ME, 17-20 July 2006, 2006, pp. 51–59. http://dx.doi.org/10.1145/1147403.1147413
  12. N. Kaveh, “Using Model Checking to Detect Deadlocks in Distributed Object Systems,” in 2nd International Workshop on Distributed Objects, Davis, CA, 2-3 November 2000, LNCS vol.1999, 2001, pp. 116–128. http://dx.doi.org/10.1007/3-540-45254-0_11
  13. J. Cho, J. Yoo, and S. Cha, “NuEditor – A Tool Suite for Specification and Verification of NuSCR,” in Lecture Notes in Computer Science vol. 3647, Berlin Heidelberg: Springer, 2006, pp. 19–28. http://dx.doi.org/10.1007/11668855_2
  14. O. Inverso, T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato, “Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs,” in 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), Lincoln, NE, 9-13 November 2015, 2015, pp. 807–812. http://dx.doi.org/10.1109/ASE.2015.108
  15. Y. Yang, X. Chen, and G. Gopalakrishnan, “Inspect: A Runtime Model Checker for Multithreaded C Programs", Report UUCS-08-004, University of Utah, Salt Lake City, UT, 2008, http://www.cs.utah.edu/docs/techreports/2008/pdf/UUCS-08-004.pdf
  16. P. C. Attie, “Synthesis of large dynamic concurrent programs from dynamic specifications,” Form. Methods Syst. Des., vol. 47, no. 131, pp. 1–54, Jun. 2016. http://dx.doi.org/10.1007/s10703-016-0252-9
  17. D. Fahland, C. Favre, J. Koehler, N. Lohmann, H. Völzer, and K. Wolf, “Analysis on demand: Instantaneous soundness checking of industrial business process models,” Data Knowl. Eng., vol. 70, no. 5, pp. 448–466, May 2011. http://dx.doi.org/10.1016/j.datak.2011.01.004
  18. S. J. C. Joosten, F. V. Julien, and J. Schmaltz, “WickedXmas: Designing and Verifying on-chip Communication Fabrics,” in 3rd International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS’14, Lausanne, Switzerland, October 20, 2014, 2014, pp. 1–8. https://pure.tue.nl/ws/files/3916267 /889737443709527.pdf
  19. S. Duri, U. Buy, R. Devarapalli, and S. M. Shatz, “Application and experimental evaluation of state space reduction methods for deadlock analysis in Ada,” ACM Trans. Softw. Eng. Methodol., vol. 3, no. 4, pp. 340–380, Oct. 1994. http://dx.doi.org/10.1145/201024.201038
  20. X. Guan, Y. Li, J. Xu, C. Wang, and S. Wang, “A Literature Review of Deadlock Prevention Policy Based on Petri Nets for Automated Manufacturing Systems,” Int. J. Digit. Content Technol. its Appl., vol. 6, no. 21, pp. 426–433, Nov. 2012. http://dx.doi.org/10.4156/jdcta.vol6.issue21.48
  21. M. A. Reniers and T. A. C. Willemse, “Folk Theorems on the Correspondence between State-Based and Event-Based Systems,” in 37th Conference on Current Trends in Theory and Practice of Computer Science, Nový Smokovec, Slovakia, January 22-28, 2011, 2011, pp. 494–505. http://dx.doi.org/10.1007/978-3-642-18381-2_41
  22. W. Penczek, M. Szreter, R. Gerth, and R. Kuiper, “Improving Partial Order Reductions for Universal Branching Time Properties,” Fundam. Informaticae, vol. 43, no. 1–4, pp. 245–267, 2000. http://dx.doi.org/10.3233/FI-2000-43123413
  23. W. Jia and W. Zhou, Distributed Network Systems. From Concepts to Implementations. New York: Springer, 2005. http://dx.doi.org/10.1007/b102545
  24. B. Czejdo, S. Bhattacharya, M. Baszun, and W. B. Daszczuk, “Improving Resilience of Autonomous Moving Platforms by real-time analysis of their Cooperation,” Autobusy-TEST, vol. 17, no. 6, pp. 1294–1301, 2016. https://arxiv.org/abs/ 1705.04263
  25. W. B. Daszczuk, “Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems,” in 23rd International Symposium on Methodologies for Intelligent Systems, ISMIS 2017, Warsaw, Poland, 26-29 June 2017, Studies in Big Data, vol. 40, Bembenik, R. et al., Eds, Cham, Switzerland: Springer International Publishing, 2019. pp. 115-129. http://dx.doi.org/10.1007/978-3-319-77604-0_9
  26. M. Schwarick, M. Heiner, and C. Rohr, “MARCIE - Model Checking and Reachability Analysis Done EffiCIEntly,” in 2011 Eighth International Conference on Quantitative Evaluation of SysTems, Aachen, Germany, 5-8 Sept. 2011, 2011, pp. 91–100. http://dx.doi.org/10.1109/QEST.2011.19
  27. Charlie, http://www-dssz.informatik.tu-cottbus.de/DSSZ/Software/Charlie
  28. M. Heiner, M. Schwarick, and J.-T. Wegener, “Charlie – An Extensible Petri Net Analysis Tool,” in 36th International Conference, PETRI NETS 2015, Brussels, Belgium, 21-26 June 2015, 2015, pp. 200–211. http://dx.doi.org/10.1007/978-3-319-19488-2_10
  29. Z. Li and M. Zhou, “Elementary Siphons of Petri Nets and Their Application to Deadlock Prevention in Flexible Manufacturing Systems,” IEEE Trans. Syst. Man, Cybern. - Part A Syst. Humans, vol. 34, no. 1, pp. 38–51, Jan. 2004. http://dx.doi.org/10.1109/TSMCA.2003.820576
  30. M. H. Abdul-Hussin, "Elementary Siphons of Petri Nets and Deadlock Control in FMS", J. of Comput. Commun., vol.3, No.7, pp. 1–12, Jul 2015. http://dx.doi.org/10.4236/jcc.2015.37001
  31. G. Behrmann, A. David, K. G. Larsen, P. Pettersson, and W. Yi, “Developing UPPAAL over 15 years,” Softw. Pract. Exp., vol. 41, no. 2, pp. 133–142, Feb. 2011. http://dx.doi.org/10.1002/spe.1006
  32. T. Latvala, A. Biere, K. Heljanko, and T. Junttila, “Simple Bounded LTL Model Checking,” in International Conference on Formal Methods in Computer-Aided Design, Austin, TX, 15-17 Nov 2004, LNCS 3312, 2004, pp. 186–200. http://dx.doi.org/10.1007/978-3-540-30494-4_14
  33. W. M. P. van der Aalst, “Workflow Verification: Finding Control-Flow Errors Using Petri-Net-Based Techniques,” in Business Process Management, LNCS vol.1806, W. van der Aalst, J. Desel, and A. Oberweis, Eds. Berlin Heidelberg: Springer, 2000, pp. 161–183. http://dx.doi.org/10.1007/3-540-45594-9_11
  34. M. Yamauchi and T. Watanabe, “Time Complexity Analysis of the Minimal Siphon Extraction Problem of Petri Nets,” IEICE Trans. Fundam. Electron. Commun. Comput. Sci., vol. E82–A, no. 11, pp. 2558–2565, 1999.
  35. F. Tricas and J. Ezpeleta, “Computing minimal siphons in Petri net models of resource allocation systems: a parallel solution,” IEEE Trans. Syst. Man, Cybern. - Part A Syst. Humans, vol. 36, no. 3, pp. 532–539, May 2006. http://dx.doi.org/10.1109/TSMCA.2005.855751
  36. P. Schnoebelen, “The complexity of temporal logic model checking,” in 4th Conference Advances in Modal Logic (AiML’2002), Toulouse, France, 30 Sept - 2 Oct 2004, Advances in Modal Logic vol. 4, 2003, pp. 437–459. http://www.aiml.net/volumes/volume4/Schnoebelen.ps
  37. R. Klimek and P. Szwed, “Verification of ArchiMate process specifications based on deductive temporal reasoning,” in FEDCSIS 2013 - Federated Conference on Computer Science and Information Systems, Kraków, Poland, 8-11 Sept 2013, 2013, pp. 1109–1116. https://ieeexplore.ieee.org/document/6644153/
  38. P. Szwed, “Efficiency of formal verification of ArchiMate business processes with NuSMV model checker,” in FEDCSIS 2015 - Federated Conference on Computer Science and Information Systems, Łódz, Poland, 13-16 Sept 2015, 2015, pp. 1427–1436. http://dx.doi.org/10.15439/2015F44
  39. A. T. E. Dib and Z. Sahnoun, “Model Checking of Multi Agent System Architectures Using BigMC,” in FEDCSIS 2015 - Federated Conference on Computer Science and Information Systems, Łódź, Poland, 13-16 Sept 2015, 2015, pp. 1717–1722. http://dx.doi.org/10.15439/2015F300
  40. F. Cicirelli, A. Furfaro, L. Nigro, and F. Pupo, “Modelling Java Concurrency: An Approach and a UPPAAL Library,” in FEDCSIS 2013 - Federated Conference on Computer Science and Information Systems, Kraków, Poland, 8-11 Sept 2013, 2013, pp. 1373–1380, https://ieeexplore.ieee.org/document/6644196