Abstract
In this paper, we suggest three optimizations to the L*-based automated Assume-Guarantee reasoning algorithm for the compositional verification of concurrent systems. First, we use each counterexample from the model checker to supply multiple strings to L*, saving candidate queries. Second, we observe that in existing instances of this paradigm, the learning algorithm is coupled weakly with the teacher. Thus, the learner ignores completely the details about the internal structure of the system and specification being verified, which are available already to the teacher. We suggest an optimization that uses this information in order to avoid many unnecessary – and expensive, since they involve model checking – membership and candidate queries. Finally, and most importantly, we develop a method for minimizing the alphabet used by the assumption, which reduces the size of the assumption and the number of queries required to construct it. We present these three optimizations in the context of verifying trace containment for concurrent systems composed of finite state machines. We have implemented our approach and experimented with real-life examples. Our results exhibit an average speedup of over 12 times due to the proposed improvements.
This research was supported by the Predictable Assembly from Certifiable Components (PACC) initiative at the Software Engineering Institute, Pittsburgh, USA.
Chapter PDF
Similar content being viewed by others
References
Păsăreanu, C.S., Giannakopoulou, D., Cobleigh, J.M.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation (2) (1987)
Wallnau, K., et al.: The ComFoRT Reasoning Framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 164–169. Springer, Heidelberg (2005)
Rivest, R.L., Schapire, R.E.: Inference of Finite Automata Using Homing Sequences. Information and Computation (2) (1993)
Peled, D., Vardi, M., Yannakakis, M.: Black box checking. In: Proc. of FORTE (1999)
Peled, D.A., Yannakakis, M., Groce, A.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, Springer, Heidelberg (2002)
Alur, R., et al.: Synthesis of Interface Specifications for Java Classes. In: POPL (2005)
Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proc. of INFINITY (2005)
Ernst, M., et al.: Dynamically Discovering Likely Program Invariants to Support Program Evolution. In: Proc. of ICSE (1999)
Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 548–562. Springer, Heidelberg (2005)
Clarke, E., et al.: Automated Assume-Guarantee Reasoning for Simulation Conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 534–547. Springer, Heidelberg (2005)
Chaki, S., Sinha, N.: Assume-guarantee reasoning for deadlock. In: Proc. of FMCAD (2006)
Giannakopoulou, D.: Assumption Generation for Software Component Verification. In: Proc. of ASE (2002)
Pnueli, A.: In Transition from Global to Modular Temporal Reasoning About Programs. In: Logics and Models of Concurrent Systems (1985)
Kurshan, R.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Clarke, E., et al.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM (JACM) 50(5) (2003)
Ball, T., Rajamani, S.: Generating Abstract Explanations of Spurious Counterexamples in C Programs. Technical Report MSR-TR-2002-09, Microsoft (2002)
Păsăreanu, C.S., Giannakopoulou, D., Gheorghiu, M.D.: Refining Interface Alphabets for Compositional Verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 292–307. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Chaki, S., Strichman, O. (2007). Optimized L*-Based Assume-Guarantee Reasoning. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)