Skip to main content
SpringerLink
Log in

2-Vagabonds: Non-exhaustive Verification Algorithm

  • Chapter
  • First Online:
Book cover Integrated Model of Distributed Systems

Part of the book series: Studies in Computational Intelligence ((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.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

  • 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.

  • 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.

  • 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.

    Article  Google Scholar 

  • 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.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

  • 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.

    Article  Google Scholar 

  • 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.

  • 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.

  • 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.

  • 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.

  • 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.

  • 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.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

  • 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.

  • 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.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

    Article  MATH  Google Scholar 

  • 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.

  • Milner, R. (1984). A calculus of communicating systems (Vol. 92, LNCS). Berlin, Heidelberg: Springer. https://doi.org/10.1007/3-540-10235-3

    MATH  Google Scholar 

  • 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.

  • 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.

  • 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.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

    Article  MathSciNet  MATH  Google Scholar 

  • 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.

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Warsaw University of Technology, Warsaw, Poland

    Wiktor B. Daszczuk

Authors
  1. Wiktor B. Daszczuk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wiktor B. Daszczuk .

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Daszczuk, W.B. (2020). 2-Vagabonds: Non-exhaustive Verification Algorithm. In: Integrated Model of Distributed Systems. Studies in Computational Intelligence, vol 817. Springer, Cham. https://doi.org/10.1007/978-3-030-12835-7_11

Download citation

Publish with us

Policies and ethics

Search

Navigation