Fei He
ABSTRACT
Both symbolic model checking and assume-guarantee reasoning aim to circumvent the state explosion problem. Symbolic model checking explores many states simultaneously and reports numerous erroneous traces. Automated assume-guarantee reasoning, on the other hand, infers contextual assumptions by inspecting spurious erroneous traces. One would expect that their integration could further improve the capacity of model checking. Yet examining numerous erroneous traces to deduce contextual assumptions can be very time-consuming. The integration of symbolic model checking and assume-guarantee reasoning is thus far from clear. In this paper, we present a progressive witness analysis algorithm for automated assume-guarantee reasoning to exploit a multitude of traces from BDD-based symbolic model checkers. Our technique successfully integrates symbolic model checking with automated assume-guarantee reasoning by directly inferring BDD's as implicit assumptions. It outperforms monolithic symbolic model checking in four benchmark problems and an industrial case study in experiments.
- R. Alur, P. Madhusudan, and W. Nam. Symbolic compositional verification by learning assumptions. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, volume 3576 of Lecture Notes in Computer Science, pages 548–562. Springer, 2005. Google Scholar
Digital Library
- D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87–106, November 1987. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, and V. Singh. Algorithms for interface synthesis. In W. Damm and H. Hermanns, editors, Computer Aided Verification, volume 4590 of Lecture Notes in Computer Science, pages 4–19. Springer, 2007. Google ScholarDigital Library
- B. Bollig, P. Habermehl, C. Kern, and M. Leucker. Angluin-style learning of NFA. In C. Boutilier, editor, International Joint Conferences on Artificial Intelligence, pages 1004–1009, 2009. Google ScholarDigital Library
- A. J. N. Brad J. Cox. Object-Oriented Programming: An Evolutionary Approach. Addison-Wesley, 1991. Google ScholarDigital Library
- N. H. Bshouty. Exact learning Boolean function via the monotone theory. Information and Computation, 123(1):146–153, 1995. Google ScholarDigital Library
- J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10 20 states and beyond. Information and Computation, 98(2):142–170, June 1992. Google ScholarDigital Library
- S. Chaki, E. M. Clarke, N. Sinha, and P. Thati. Automated assume-guarantee reasoning for simulation conformance. In K. Etessami and S. K. Rajamani, editors, Computer Aided Verification, volume 3576 of Lecture Notes in Computer Science, pages 534–547. Springer, 2005. Google ScholarDigital Library
- S. Chaki and O. Strichman. Optimized L ∗ -based assume-guarantee reasoning. In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 276–291. Springer, 2007. Google ScholarDigital Library
- D. Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology, 1(1):65–75, 1988. Google ScholarCross Ref
- Y.-F. Chen, E. M. Clarke, A. Farzan, F. He, M.-H. Tsai, Y.-K. Tsay, B.-Y. Wang, and L. Zhu. Comparing learning algorithms in automated assume-guarantee reasoning. In Leveraging Applications of Formal Methods, Verification and Validation (1), volume 6415 of Lecture Notes in Computer Science, pages 643–657. Springer, 2010. Google ScholarDigital Library
- Y.-F. Chen, E. M. Clarke, A. Farzan, M.-H. Tsai, Y.-K. Tsay, and B.-Y. Wang. Automated assume-guarantee reasoning through implicit learning. In T. Touili, B. Cook, and P. Jackson, editors, Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 511–526. Springer, 2010. Google ScholarDigital Library
- Y.-F. Chen, A. Farzan, E. M. Clarke, Y.-K. Tsay, and B.-Y. Wang. Learning minimal separating DFA’s for compositional verification. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of Lecture Notes in Computer Science, pages 31–45. Springer, 2009. Google ScholarDigital Library
- Y.-F. Chen and B.-Y. Wang. Learning boolean functions incrementally. In M. Parthasarathy and S. A. Seshia, editors, Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, pages 55–70. Springer, 2012. Google ScholarDigital Library
- A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: a new Symbolic Model Verifier. In N. Halbwachs and D. Peled, editors, Computer Aided Verification, number 1633 in Lecture Notes in Computer Science, pages 495–499. Springer, 1999. Google ScholarDigital Library
- E. M. Clarke, E. A. Emerson, and J. Sifakis. Model checking: Algorithmic verification and debugging. Communications of ACM, 52(11):74–84, 2009. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752–794, 2003. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. Google ScholarDigital Library
- J. M. Cobleigh, G. S. Avrunin, and L. A. Clarke. Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Trans. Software Engineering Methodology, 17(2), 2008. Google ScholarDigital Library
- J. M. Cobleigh, D. Giannakopoulou, and C. S. Păsăreanu. Learning assumptions for compositional verification. In H. Garavel and J. Hatcliff, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2619 of Lecture Notes in Computer Science, pages 331–346. Springer, 2003. Google ScholarDigital Library
- W.-P. de Roever, F. de Boer, U. Hanneman, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Number 54 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In Principles of Programming Languages, pages 191–202. ACM, 2002. Google ScholarDigital Library
- R. Gavaldà and D. Guijarro. Learning ordered binary decision diagrams. In K. P. Jantke, T. Shinohara, and T. Zeugmann, editors, Algorithmic Learning Theory, volume 997 of Lecture Notes in Computer Science, pages 228–238. Springer, 1995. Google ScholarDigital Library
- M. Gheorghiu, D. Giannakopoulou, and C. S. Păsăreanu. Refining interface alphabets for compositional verification. In O. Grumberg and M. Huth, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 292–307. Springer, 2007. Google ScholarDigital Library
- D. Giannakopoulou and C. S. Păsăreanu. Special issue on learning techniques for compositional reasoning. Formal Methods in System Design, 32(3):173–174, 2008. Google ScholarDigital Library
- A. Gupta, K. L. McMillan, and Z. Fu. Automated assumption generation for compositional verification. In W. Damm and H. Hermanns, editors, Computer Aided Verification, volume 4590 of Lecture Notes in Computer Science, pages 420–432. Springer, 2007. Google ScholarDigital Library
- A. Gupta, K. L. McMillan, and Z. Fu. Automated assumption generation for compositional verification. Formal Methods in System Design, 32(3):285–301, 2008. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, and R. Majumdar. Permissive interfaces. In Foundations of Software Engineering, ESEC/FSE-13, pages 31–40. ACM, 2005. Google ScholarDigital Library
- M. J. Kearns and U. V. Vazirani. An Introduction to Computational Learning Theory. MIT Press, 1994. Google ScholarCross Ref
- B. Meyer. Object-Oriented Software Construction. Prentice Hall, 1997. Google ScholarDigital Library
- A. Nakamura. An efficient query learning algorithm for ordered binary decision diagrams. Information and Computation, 201(2):178–198, 2005. Google ScholarDigital Library
- W. Nam, P. Madhusudan, and R. Alur. Automatic symbolic compositional verification by learning assumptions. Formal Methods in System Design, 32(3):207–234, 2008. Google ScholarDigital Library
- H. Sa´ıdi and S. Graf. Construction of abstract state graphs with PVS. In Grumberg, editor, Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 72–83. Springer, 1997. Google ScholarDigital Library
- R. Singh, D. Giannakopoulou, and C. S. Pasareanu. Learning component interfaces with may and must abstractions. In T. Touili, B. Cook, and P. Jackson, editors, Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 527–542. Springer, 2010. Google ScholarDigital Library
- N. Sinha and E. M. Clarke. SAT-based compositional verification using lazy learning. In W. Damm and H. Hermanns, editors, Computer Aided Verification, volume 4590 of Lecture Notes in Computer Science, pages 39–54. Springer, 2007. Google ScholarDigital Library
- L. Théry. Proof pearl: Revisiting the mini-Rubik in Coq. In O. A. Mohamed, C. Mu˜ noz, and S. Tahar, editors, Theorem Proving in Higher Order Logics, volume 5170 of Lecture Notes in Computer Science, pages 310–319. Springer, 2008. Google ScholarDigital Library
- R. Wang, M. Zhou, L. Yin, L. Zhang, J. Sun, G. Ming, and M. Bozga. Modeling and validation of PLC-controlled systems: A case study. In Theoretical Aspects of Software Engineering, pages 161–166. IEEE, 2012. Google ScholarDigital Library
Index Terms
- Symbolic assume-guarantee reasoning through BDD learning
Recommendations
Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process
Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and ...
Automatic symbolic compositional verification by learning assumptions
Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify ...
Counterexample-Guided Assume-Guarantee Synthesis through Learning
Assume-guarantee reasoning (AGR) is a promising compositional verification technique that can address the state space explosion problem associated with model checking. Since the construction of assumptions usually requires nontrivial human efforts, a ...
Comments