Advertisement

Deadlock Detection Examples: The Dedan Environment at Work

  • Wiktor B. DaszczukEmail author
Chapter
Part of the Studies in Computational Intelligence book series (SCI, volume 817)

Abstract

The example of deadlock detection is presented for the system in which two distributed computations, each one running on its own server, use two semaphores.

References

  1. Barbey, S., Buchs, D., & Péraire, C. (1998a). A case study for testing object-oriented software: A production cell. Url: http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.460.
  2. Barbey, S., Buchs, D., & Péraire, C. (1998b). Modelling the production cell case study using the fusion method. Lausanne, Switzerland. Url: https://infoscience.epfl.ch/record/54618/files/Barbey98-298..ps.gz.
  3. Behrmann, G., David, A., & Larsen, K. G. (2006). A tutorial on Uppaal 4.0. Aalborg, Denmark. Url: http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf.
  4. Ben-Abdallah, H., & Lee, I. (1998). A graphical language for specifying and analyzing real-time systems. Integrated Computer-Aided Engineering, 5(4), 279–302. Url: ftp://ftp.cis.upenn.edu/pub/rtg/Paper/Full_Postscript/icae97.pdf.
  5. Benghazi Akhlaki, K., Capel Tuñón, M. I., & Mendoza Morales, L. E. (2007). A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Science of Computer Programming, 65(1), 41–56.  https://doi.org/10.1016/j.scico.2006.08.005.MathSciNetCrossRefzbMATHGoogle Scholar
  6. Beyer, D., Lewerentz, C., & Noack, A. (2003). Rabbit: A tool for BDD-based verification of real-time systems. In Computer Aided Verification, CAV 2003, Boulder, CO, 8–12 July 2003, LNCS 2725 (pp. 122–125). Heidelberg: Springer.  https://doi.org/10.1007/978-3-540-45069-6_13.
  7. Beyer, D., & Rust, H. (1998). Modeling a production cell as a distributed real-time system with cottbus timed automata. In H. König & P. Langendörfer (Eds.), Formale Beschreibungstechniken für verteilte Systeme, 8. GI/ITG-Fachgespräch, Cottbus, Germany, 4–5 June 1998. München, Germany: Shaker Verlag. Url: https://www.sosy-lab.org/~dbeyer/Publications/1998-FBT.Modeling_a_Production_Cell_as_a_Distributed_Real-Time_System_with.Cottbus_Timed_Automata.pdf.
  8. Björnander, S., Seceleanu, C., … Pettersson, P. (2011). ABV—A verifier for the architecture analysis and design language (AADL). In 6th IEEE International Conference on Engineering of Complex Computer Systems, Las Vegas, NV, 27–29 April 2011 (pp. 355–360). IEEE.  https://doi.org/10.1109/iceccs.2011.43.
  9. Budde, R. (1995). Esterel. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 5 (pp. 75–100). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_49.
  10. Burghardt, J. (1995). Deductive synthesis. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 17 (pp. 295–309). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_61.
  11. Burns, A. (2003). How to verify a safe real-time system—The application of model checking and timed automata to the production cell case study. Real-Time Systems, 24(2), 135–151.  https://doi.org/10.1023/A:1021758401878.CrossRefzbMATHGoogle Scholar
  12. Capecchi, S., Giachino, E., & Yoshida, N. (2016). Global escape in multiparty sessions. Mathematical Structures in Computer Science, 26(02), 156–205.  https://doi.org/10.1017/S0960129514000164.MathSciNetCrossRefzbMATHGoogle Scholar
  13. Cardell-Oliver, R. (1995). HTTDs and HOL. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 15 (pp. 261–276). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_59.
  14. Cassez, F., David, A., … Lime, D. (2005). Efficient on-the-fly algorithms for the analysis of timed games. In 16th International Conference on Concurrency Theory (CONCUR’05), San Francisco, CA, 23–26 Aug. 2005, LNCS 3653 (pp. 66–80). Heidelberg: Springer.  https://doi.org/10.1007/11539452_9.
  15. Cattel, T. (1995). Process control design using SPIN. In Spin Workshop, Montreal, Canada, 16 Oct. 1995. Url: http://spinroot.com/spin/Workshops/ws95/cattel.pdf.
  16. Cuellar, J., & Huber, M. (1995). TLT. In C. Lewerentz & T. Lindne (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. (pp. 151–169). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_53.
  17. Czejdo, B., Bhattacharya, S., … Daszczuk, W. B. (2016). Improving resilience of autonomous moving platforms by real-time analysis of their cooperation. Autobusy-TEST, 17(6), 1294–1301. Url: http://www.autobusy-test.com.pl/images/stories/Do_pobrania/2016/nr%206/logistyka/10_l_czejdo_bhattacharya_baszun_daszczuk.pdf.
  18. Daszczuk, W. B. (2003). Verification of temporal properties in concurrent systems. Warsaw University of Technology. Url: https://repo.pw.edu.pl/docstore/download/WEiTI-0b7425b5-2375-417b-b0fa-b1f61aed0623/Daszczuk.pdf.
  19. Daszczuk, W. B., Bielecki, M., & Michalski, J. (2017). Rybu: Imperative-style preprocessor for verification of distributed systems in the Dedan environment. In KKIO’17—Software Engineering Conference, Rzeszów, Poland, 14–16 Sept. 2017. Polish Information Processing Society. arXiv:1710.02722.
  20. Daszczuk, W. B., & Mieścicki, J. (2014). Chapter 7.2 Principles of PRT network simulation. In W. Choromański (Ed.), Ecomobility. Innovative and ecological transport means (in Polish) (pp. 193–209). Wydawnictwa Komunikacji i Łączności. ISBN: 978-83-206-1953-9.Google Scholar
  21. Dierks, H. (1996). The production cell: A verified real-time system. In 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT 1996: Uppsala, Sweden, 9–13 Sept. 1996, LNCS 1135 (pp. 208–227). Heidelberg: Springer.  https://doi.org/10.1007/3-540-61648-9_42.
  22. Dijkstra, E. W. (1971). Hierarchical ordering of sequential processes. Acta Informatica, 1(2), 115–138.  https://doi.org/10.1007/BF00289519.MathSciNetCrossRefGoogle Scholar
  23. Ehlers, R., Mattmüller, R., & Peter, H.-J. (2010). Combining symbolic representations for solving timed games. In K. Chatterjee & T. A. Henzinger (Eds.), 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, Klosterneuburg, Austria, 8–10 Sept. 2010, LNCS 6246 (pp. 107–121). Heidelberg: Springer.  https://doi.org/10.1007/978-3-642-15297-9_10.
  24. Fuchs, M., & Philipps, J. (1995). Focus. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 11 (pp. 185–197). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_55.
  25. Garavel, H., & Serwe, W. (2017). The unheralded value of the multiway rendezvous: Illustration with the production cell benchmark. Electronic Proceedings in Theoretical Computer Science, 244, 230–270.  https://doi.org/10.4204/EPTCS.244.10.CrossRefGoogle Scholar
  26. Greenyer, J., Brenner, C., … Gressi, E. (2013). Incrementally synthesizing controllers from scenario-based product line specifications. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering—ESEC/FSE 2013, Sankt Petersburg, Russia, 18–26 Aug. 2013 (pp. 433–443). New York: ACM Press.  https://doi.org/10.1145/2491411.2491445.
  27. Grosu, R., Broy, M., … Stefănescu, G. (1999). What is behind UML-RT? In H. Kilov, B. Rumpe, & I. Simmonds (Eds.), Behavioral specifications of businesses and systems (pp. 75–90). Boston, MA: Springer US.  https://doi.org/10.1007/978-1-4615-5229-1_6.
  28. Heiner, M., & Heisel, M. (1999). Modeling safety-critical systems with Z and petri nets. In M. Felici, K. Kanoun, & A. Pasquini (Eds.), SAFECOMP ’99 Proceedings of the 18th International Conference on Computer Safety, Reliability and Security, Toulouse, France, 27–29 Sept. 1999, LNCS Vol. 1698 (pp. 361–374). Heidelberg: Springer.  https://doi.org/10.1007/3-540-48249-0_31.
  29. Heinkel, S., & Lindner, T. (1995). SDL. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 10 (pp. 171–183). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_54.
  30. Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21(8), 666–677.  https://doi.org/10.1145/359576.359585.CrossRefzbMATHGoogle Scholar
  31. Holenderski, L. (1995). Lustre. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 6 (pp. 101–112). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_50.
  32. Jacobs, J., & Simpson, A. (2015). A formal model of SysML blocks using CSP for assured systems engineering. In Formal Techniques for Safety-Critical Systems, Third International Workshop, FTSCS 2014, Luxembourg, 6–7 Nov. 2014, Communications in Computer and Information Science 476 (pp. 127–141). Heidelberg: Springer.  https://doi.org/10.1007/978-3-319-17581-2_9.
  33. Klingenbeck, S., & Käufl, T. (1995). Tatzelwurm. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 14 (pp. 247–259). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_58.
  34. Korf, F., & Schlör, R. (1995). Symbolic timing diagrams. In C. Lewerentz & T. Lindner (Eds.), Formal development of reactive systems. LNCS Vol. 891, chapt. 18 (pp. 311–331). Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1_62.
  35. Larsen, P. G., Fitzgerald, J. S., & Riddle, S. (2009). Practice-oriented courses in formal methods using VDM++. Formal Aspects of Computing, 21(3), 245–257.  https://doi.org/10.1007/s00165-008-0068-5.CrossRefGoogle Scholar
  36. Lewerentz, C., & Lindner, T. (Eds.). (1995). Formal development of reactive systems, LNCS 891. Heidelberg: Springer.  https://doi.org/10.1007/3-540-58867-1.
  37. Ma, C., & Wonham, W. M. (2005). The production cell example. Chapter 5. In Nonblocking Supervisory Control of State Tree Structures. Lecture Notes in Control and Information Science 317 (pp. 127–144). Heidelberg: Springer.  https://doi.org/10.1007/11382119_5.
  38. Masticola, S. P., & Ryder, B. G. (1990). Static infinite wait anomaly detection in polynomial time. In 1990 International Conference on Parallel Processing, Urbana-Champaign, IL, 13–17 Aug. 1990 (Vol. 2, pp. 78–87). University Park, PA: Pennsylvania State University Press. Url: https://rucore.libraries.rutgers.edu/rutgers-lib/57963/.
  39. Milner, R. (1984). A calculus of communicating systems. Heidelberg: Springer.zbMATHGoogle Scholar
  40. Nardone, R., Gentile, U., … Mazzocca, N. (2016). Modeling railway control systems in promela (pp. 121–136).  https://doi.org/10.1007/978-3-319-29510-7_7.
  41. Pedersen, M. H., Christiansen, M. K., & Glæsner, T. (2000). Solving the priority inversion problem in legOS. Aalborg, Denmark. Url: http://www.it.uu.se/edu/course/homepage/realtid/p2ht08/lego/prioinvers.pdf.
  42. Priority Inversion and Deadlock. Whitepaper. (2011). Url: https://code-time.com/pdf/Priority%20Inversion%20and%20Deadlock.pdf.
  43. Ramakrishnan, S., & McGregor, J. (2000). Modelling and testing OO distributed systems with temporal logic formalisms. In 8th International IASTED Conference Applied Informatics’ 2000, Innsbruck, Austria, 14–17 Feb. 2000. Url: https://research.monash.edu/en/publications/modelling-and-testing-oo-distributed-systems-with-temporal-logic-.
  44. Rosa, N. S., & Cunha, P. R. F. (2004). A software architecture-based approach for formalising middleware behaviour. Electronic Notes in Theoretical Computer Science, 108, 39–51.  https://doi.org/10.1016/j.entcs.2004.01.011.CrossRefGoogle Scholar
  45. Ruf, J., & Kropf, T. (1999). Modeling and checking networks of communicating real-time processes. In L. Pierre & T. Kropf (Eds.), CHARME’99, Advanced Research Working Conference on Correct Hardware Design and Verification Methods, BadHerrenalb, Germany, 27–29 Sept. 1999, LNCS 1703 (pp. 267–279). Heidelberg: Springer.  https://doi.org/10.1007/3-540-48153-2_20.
  46. Schröter, C., Schwoon, S., & Esparza, J. (2003). The model-checking kit. In 24th International Conference ICATPN 2003: Eindhoven, The Netherlands, June 23–27, 2003, LNCS 2697 (pp. 463–472). Heidelberg: Springer.  https://doi.org/10.1007/3-540-44919-1_29.
  47. Sebesta, R. W. (1996). Concepts of programming languages. Reading, MA: Addison-Wesley Publishing Compan.zbMATHGoogle Scholar
  48. Sokolsky, O., Lee, I., & Ben-Abdallah, H. (1999). Specification and analysis of real-time systems with PARAGON (equivalence checking). Philadelphia, PA. Url: https://www.cis.upenn.edu/~sokolsky/ase99.pdf.
  49. Tai, K. (1994). Definitions and detection of deadlock, livelock, and starvation in concurrent programs. In D. P. Agrawal (Ed.), 1994 International Conference on Parallel Processing (ICPP’94), Raleigh, NC, 15–19 Aug. 1994 (pp. 69–72). Boca Raton: CRC Press.  https://doi.org/10.1109/icpp.1994.84.
  50. Vu, L. H., Haxthausen, A. E., & Peleska, J. (2015). Formal modeling and verification of interlocking systems featuring sequential release (pp. 223–238).  https://doi.org/10.1007/978-3-319-17581-2_15.
  51. Waeselynck, H., & Thévenod-Fosse, P. (1999). A case study in statistical testing of reusable concurrent objects. In J. Hlavička, E. Maehle, & A. Pataricza (Eds.), Third European Dependable Computing Conference, Prague, Czech Republic, 15–17 Sept. 1999, LNCS 1667 (pp. 401–418). Heidelberg: Springer.  https://doi.org/10.1007/3-540-48254-7_27.
  52. Žic, J. J. (1994). Time-constrained buffer specifications in CSP+T and timed CSP. ACM Transactions on Programming Languages and Systems, 16(6), 1661–1674.  https://doi.org/10.1145/197320.197322.CrossRefGoogle Scholar
  53. Zorzo, A. F., Romanovsky, A., … Welch, I. S. (1999). Using coordinated atomic actions to design safety-critical systems: a production cell case study. Software: Practice and Experience, 29(8), 677–697.  https://doi.org/10.1002/(sici)1097-024x(19990710)29:8%3c677::aid-spe251%3e3.0.co;2-z.

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of Computer ScienceWarsaw University of TechnologyWarsawPoland

Personalised recommendations