Advertisement

2-Vagabonds: Non-exhaustive Verification Algorithm

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

Abstract

Static deadlock detection methods suffer from space explosion problem. Model checking and other static analysis techniques are very effective in verification, many of them have a linear complexity to the size of the reachability space. However, the elaboration of the space is time-consuming (usually exponential) and takes a large amount of memory.

References

  1. Alba, E., & Chicano, F. (2007). Ant colony optimization for model checking. In R. Moreno Díaz, F. Pichler, & A. Quesada Arencibia (Eds.), International Conference on Computer Aided Systems Theory—EUROCAST 2007, Las Palmas, Spain, LNCS (Vol. 4739, pp. 523–530), 12–16 February, 2007. Berlin Heidelberg: Springer.  https://doi.org/10.1007/978-3-540-75867-9_66.
  2. Alba, E., & Troya, J. M. (1996). Genetic algorithms for protocol validation. In H.-M. Voigt, W. Ebeling, I. Rechenberg, & H.-P. Schwefel (Eds.), International Conference on Parallel Problem Solving from Nature PPSN 1996—PPSN IV, Berlin, Germany (pp. 869–879), 22–26 September, 1996. Berlin, Heidelberg: Springer.  https://doi.org/10.1007/3-540-61723-x_1050.
  3. Batista, G. E. A. P. A., Prati, R. C., & Monard, M. C. (2004). A study of the behavior of several methods for balancing machine learning training data. ACM SIGKDD Explorations Newsletter, 6(1), 20–29.  https://doi.org/10.1145/1007730.1007735.CrossRefGoogle Scholar
  4. Chicano, F., & Alba, E. (2008). Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models. Information Processing Letters, 106(6), 221–231.  https://doi.org/10.1016/j.ipl.2007.11.015.MathSciNetCrossRefzbMATHGoogle Scholar
  5. Clarke, E. M., Long, D. E., & McMillan, K. L. (1989). Compositional model checking. In Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, CA (pp. 353–362), 5–8 June 1989. IEEE Computer Society Press.  https://doi.org/10.1109/lics.1989.39190.
  6. Clarke, E. M., Grumberg, O., & Long, D. E. (1994). Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1512–1542.  https://doi.org/10.1145/186025.186051.CrossRefGoogle Scholar
  7. Clarke, E., McMillan, K., Campos, S., & Hartonas-Garmhausen, V. (1996). Symbolic model checking. In R. Alur & T. A. Henzinger (Eds.), 8th International Conference on Computer Aided Verification—CAV’96, New Brunswick, NJ (pp. 419–422), 31 July–3 August, 1996. Berlin, Heidelberg: Springer.  https://doi.org/10.1007/3-540-61474-5_93.
  8. Czejdo, B., Bhattacharya, S., Baszun, M., & 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.
  9. Daszczuk, W. B. (2018a). Siphon-based deadlock detection in integrated model of distributed systems (IMDS). In Federated Conference on Computer Science and Information Systems, 3rd Workshop on Constraint Programming and Operation Research Applications (CPORA’18), Poznań, Poland (pp. 421–431), 9–12 September, 2018. IEEE.  https://doi.org/10.15439/2018f114.
  10. Daszczuk W B. (2019a). Asynchronous specification of production cell benchmark in integrated model of distributed systems. In R. Bembenik, L. Skonieczny, G. Protaziuk, M. Kryszkiewicz, & H. Rybinski (Eds.), 23rd International Symposium on Methodologies for Intelligent Systems, ISMIS 2017, Warsaw, Poland, Studies in Big Data (Vol. 40, pp. 115–129), 26–29 June, 2017. Cham, Switzerland: Springer International Publishing.  https://doi.org/10.1007/978-3-319-77604-0_9.
  11. Daszczuk, W. B. (2019b). Fairness in temporal verification of distributed systems. In W. Zamojski, J. Mazurkiewicz, J. Sugier, T. Walkowiak, & J. Kacprzyk (Eds.), 13th International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, Brunów, Poland, AISC (Vol. 761, pp. 135–150), 2–6 July, 2018. Cham, Switzerland: Springer International Publishing.  https://doi.org/10.1007/978-3-319-91446-6_14.
  12. Dijkstra, E. W. (1959). A note on two problems in connexion with graphs. Numerische Mathematik, 1(1), 269–271.  https://doi.org/10.1007/BF01386390.MathSciNetCrossRefzbMATHGoogle Scholar
  13. Francesca, G., Santone, A., Vaglini G., & Villani, M. L. (2011). Ant colony optimization for deadlock detection in concurrent systems. In 2011 IEEE 35th Annual Computer Software and Applications Conference, Munich, Germany (pp. 108–117), 18–22 July, 2011. IEEE.  https://doi.org/10.1109/compsac.2011.22.
  14. Godefroid, P., & Khurshid, S. (2002). Exploring Very Large State Spaces Using Genetic Algorithms. In J.-P. Katoen & P. Stevens (Eds.), International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS 2002, Grenoble, France, LNCS (Vol. 2280, pp. 266–280), 8–12 April, 2002. Berlin Heidelberg: Springer.  https://doi.org/10.1007/3-540-46002-0_19.
  15. Gradara, S., Santone, A., & Villani, M. L. (2006). DELFIN+: An efficient deadlock detection tool for CCS processes. Journal of Computer and System Sciences, 72(8), 1397–1412.  https://doi.org/10.1016/j.jcss.2006.03.003.MathSciNetCrossRefzbMATHGoogle Scholar
  16. Hatcliff, J., Dwyer, M. B., & Zheng, H. (2000). Slicing software for model construction. Higher-Order and Symbolic Computation, 13(4), 315–353.  https://doi.org/10.1023/A:1026599015809.CrossRefzbMATHGoogle Scholar
  17. Jard C, and Jéron T. (1992). Bounded-memory algorithms for verification on-the-fly. In International Conference on Computer Aided Verification—CAV 1991, Aalborg, Denmark (pp. 192–202), 1–4 July, 1991. Berlin Heidelberg: Springer.  https://doi.org/10.1007/3-540-55179-4_19.
  18. Milner, R. (1984). A calculus of communicating systems (Vol. 92, LNCS). Berlin, Heidelberg: Springer.  https://doi.org/10.1007/3-540-10235-3zbMATHGoogle Scholar
  19. Penczek, W., Gerth, R., Kuiper, R., Szreter, M. (1999). Partial order reductions preserving simulations. In Concurrency Specification and Programming (CS&P), Warsaw, Poland (pp. 153–171), 28–30 September, 1999. url: http://content.iospress.com/articles/fundamenta-informaticae/fi43-1-4-13.
  20. Pira, E., Rafe, V., & Nikanjam, A. (2017). Deadlock detection in complex software systems specified through graph transformation using Bayesian optimization algorithm. Journal of Systems and Software, 131, 181–200.  https://doi.org/10.1016/j.jss.2017.05.128.
  21. Santone, A. (2002). Automatic verification of concurrent systems using a formula-based compositional approach. Acta Informatica, 38(8), 531–564.  https://doi.org/10.1007/s00236-002-0084-5.MathSciNetCrossRefzbMATHGoogle Scholar
  22. Stirling, C., & Walker, D. (1991). Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1), 161–177.  https://doi.org/10.1016/0304-3975(90)90110-4.MathSciNetCrossRefzbMATHGoogle Scholar
  23. Yousefian, R., Rafe, V., & Rahmani, M. (2014). A heuristic solution for model checking graph transformation systems. Applied Soft Computing, 24, 169–180.  https://doi.org/10.1016/j.asoc.2014.06.055.

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of Computer ScienceWarsaw University of TechnologyWarsawPoland

Personalised recommendations