Advertisement

Exploiting Symmetry for Efficient Verification of Infinite-State Component-Based Systems

  • Qiang WangEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)

Abstract

In this paper we present an efficient verification algorithm for infinite-state component-based systems modeled in the behavior-interaction-priority (\(\textsc {BIP}\)) framework. Our algorithm extends the persistent set partial order reduction by taking into account system symmetries, and further combines it with lazy predicate abstraction. We have implemented the new verification algorithm in our model checker for \(\textsc {BIP}\). The experimental evaluation shows that for systems exhibiting certain symmetries, our new algorithm outperforms the existing algorithms significantly.

Keywords

Model Check Label Transition System Symmetry Reduction Orbit Relation Predicate Abstraction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

I wish to express my sincere gratitude to Prof. Joseph Sifakis for his inspirations on \(\textsc {BIP}\), and to Dr. Alessandro Cimatti, Dr. Marco Roveri, Dr. Sergio Mover for their instructive guidance and help with Kratos model checker, and to Dr. Rongjie Yan, Dr. Simon Bliudze for the discussion and proofreading this manuscript, and all the anonymous reviewers for their careful reading of the paper.

References

  1. 1.
    Abdellatif, T., Bensalem, S., Combaz, J., de Silva, L., Ingrand, F.: Rigorous design of robot software: a formal component-based approach. Robot. Auton. Syst. 60, 1563–1578 (2012)CrossRefGoogle Scholar
  2. 2.
    Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  3. 3.
    Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28, 41–48 (2011)CrossRefGoogle Scholar
  4. 4.
    Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. STTT 14, 53–72 (2012)CrossRefGoogle Scholar
  5. 5.
    Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02658-4_45 CrossRefGoogle Scholar
  6. 6.
    Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-Finder 2: towards efficient correctness of incremental design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 453–458. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-20398-5_32 CrossRefGoogle Scholar
  7. 7.
    Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326–343. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-24953-7_25 CrossRefGoogle Scholar
  8. 8.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-18275-4_7 CrossRefGoogle Scholar
  9. 9.
    Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46–61. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54862-8_4 CrossRefGoogle Scholar
  10. 10.
    Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking with explicit scheduler and symbolic threads. Log. Meth. Comput. Sci. 8(2) (2012). doi: 10.2168/LMCS-8(2:18)2012
  11. 11.
    Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 147–158. Springer, Heidelberg (1998). doi: 10.1007/BFb0028741 CrossRefGoogle Scholar
  12. 12.
    Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods Syst. Des. 9, 77–104 (1996)CrossRefGoogle Scholar
  13. 13.
    Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2, 279–287 (1999)CrossRefzbMATHGoogle Scholar
  14. 14.
    Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999). doi: 10.1007/3-540-48683-6_16 CrossRefGoogle Scholar
  15. 15.
    Donaldson, A.F., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des. 41, 25–44 (2012)CrossRefzbMATHGoogle Scholar
  16. 16.
    Emerson, E.A., Jha, S., Peled, D.: Combining partial order and symmetry reductions. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 19–34. Springer, Heidelberg (1997). doi: 10.1007/BFb0035378 CrossRefGoogle Scholar
  17. 17.
    Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods Syst. Des. 9, 105–131 (1996)CrossRefGoogle Scholar
  18. 18.
    Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999). doi: 10.1007/3-540-48153-2_12 CrossRefGoogle Scholar
  19. 19.
    Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005). doi: 10.1007/978-3-540-31980-1_25 CrossRefGoogle Scholar
  20. 20.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL (2005)Google Scholar
  21. 21.
    Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. ACM SIGPLAN Not. 37, 191–202 (2002). ACMCrossRefzbMATHGoogle Scholar
  22. 22.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, New York (1996)CrossRefzbMATHGoogle Scholar
  23. 23.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). doi: 10.1007/3-540-63166-6_10 CrossRefGoogle Scholar
  24. 24.
    He, F., Yin, L., Wang, B.-Y., Zhang, L., Mu, G., Meng, W.: VCS: a verifier for component-based systems. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 478–481. Springer, Heidelberg (2013). doi: 10.1007/978-3-319-02444-8_39 CrossRefGoogle Scholar
  25. 25.
    Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. ACM SIGPLAN Not. 39, 232–244 (2004). ACMCrossRefzbMATHGoogle Scholar
  26. 26.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not. 37, 58–70 (2002)CrossRefzbMATHGoogle Scholar
  27. 27.
    Iosif, R.: Symmetry reductions for model checking of concurrent dynamic software. STTT 6, 302–319 (2004)CrossRefGoogle Scholar
  28. 28.
    Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9, 41–75 (1996)CrossRefGoogle Scholar
  29. 29.
    Konnov, I., Kotek, T., Wang, Q., Veith, H., Bliudze, S., Sifakis, J.: Parameterized systems in BIP: design and model checking. In: CONCUR (2016, to appear)Google Scholar
  30. 30.
    McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). doi: 10.1007/11817963_14 CrossRefGoogle Scholar
  31. 31.
    Miller, A., Donaldson, A., Calder, M.: Symmetry in temporal logic model checking. ACM Comput. Surv. (2006)Google Scholar
  32. 32.
    Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994). doi: 10.1007/3-540-58179-0_69 CrossRefGoogle Scholar
  33. 33.
    Sifakis, J.: Rigorous system design. Found. Trends Electron. Des. Autom. 6(4), 293–362 (2013)CrossRefGoogle Scholar
  34. 34.
    Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991). doi: 10.1007/BFb0023729 CrossRefGoogle Scholar
  35. 35.
    Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with Impact. In: FMCAD (2013)Google Scholar
  36. 36.
    Wahl, T., Donaldson, A.: Replication and abstraction: symmetry in automated formal verification. Symmetry 2, 799–847 (2010)MathSciNetCrossRefGoogle Scholar
  37. 37.
    Wang, C., Yang, Z., Kahlon, V., Gupta, A.: Peephole partial order reduction. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 382–396. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_29 CrossRefGoogle Scholar
  38. 38.
    Qiang, W., Bliudze, S.: Verification of component-based systems via predicate abstraction and simultaneous set reduction. In: Ganty, P., Loreti, M. (eds.) TGC 2015. LNCS, vol. 9533, pp. 147–162. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-28766-9_10 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.École Polytechnique Fédérale de LausanneLausanneSwitzerland

Personalised recommendations