Abstract
Techniques for learning automata have been adapted to automatically infer assumptions in assume-guarantee compositional verification. Learning, in this context, produces assumptions and modifies them using counterexamples obtained by model checking components separately. In this process, the interface alphabets between components, that constitute the alphabets of the assumption automata, are fixed: they include all actions through which the components communicate. This paper introduces alphabet refinement, a novel technique that extends the assumption learning process to also infer interface alphabets. The technique starts with only a subset of the interface alphabet and adds actions to it as necessary until a given property is shown to hold or to be violated in the system. Actions to be added are discovered by counterexample analysis. We show experimentally that alphabet refinement improves the current learning algorithms and makes compositional verification by learning assumptions more scalable than non-compositional verification.
Chapter PDF
Similar content being viewed by others
References
Alur, R., et al.: Synthesis of interface specifications for Java classes. In: Proceedings of POPL’05, pp. 98–109 (2005)
Alur, R., et al.: MOCHA: Modularity in Model Checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)
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)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987)
Barringer, H., Giannakopoulou, D., Păsăreanu, C.S.: Proof Rules for Automated Compositional Verification through Learning. In: Proceedings of SAVCBS’03, pp. 14–21 (2003)
Strichman, O., Chaki, S.: Optimized L*-Based Assume-Guarantee Reasoning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 276–291. Springer, Heidelberg (2007)
Cheung, S.C., Kramer, J.: Checking safety properties using compositional reachability analysis. ACM Transactions on Software Engineering and Methodology 8(1), 49–78 (1999)
Clarke, E.M., et al.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional Model Checking. In: Proceedings of LICS’89, pp. 353–362 (1989)
Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking Up is Hard to Do: An Investigation of Decomposition for Assume-Guarantee Reasoning. In: Proceedings of ISSTA’06, pp. 97–108. ACM Press, New York (2006)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: 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)
Flanagan, C., Freund, S.N., Qadeer, S.: Thread-Modular Verification for Shared-Memory Programs. In: Le Métayer, D. (ed.) ESOP 2002 and ETAPS 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002)
Gheorghiu, M., Giannakopoulou, D., Păsăreanu, C.S.: Refining Interface Alphabets for Compositional Verification. RIACS Technical Report (2006)
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: Proceedings of ASE’02, pp. 3–12. IEEE Computer Society Press, Los Alamitos (2002)
Grumberg, O., Long, D.E.: Model Checking and Modular Verification. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 250–265. Springer, Heidelberg (1991)
Henzinger, T.A., Jhala, R., Majumdar, R.: Permissive Interfaces. In: Proceedings of ESEC/SIGSOFT FSE’05, pp. 31–40 (2005)
Jones, C.B.: Specification and Design of (Parallel) Programs. In: Information Processing 83: Proceedings of the IFIP 9th World Congress, pp. 321–332. North Holland, Amsterdam (1983)
Krimm, J.-P., Mounier, L.: Compositional State Space Generation from Lotos Programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 239–258. Springer, Heidelberg (1997)
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley & Sons, Chichester (1999)
Alur, R., Nam, W.: Learning-Based Symbolic Assume-Guarantee Reasoning with Automatic Decomposition. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 170–185. Springer, Heidelberg (2006)
Păsăreanu, C.S., Giannakopoulou, D.: Towards a Compositional SPIN. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 234–251. Springer, Heidelberg (2006)
Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. In: Logic and Models of Concurrent Systems, vol. 13, pp. 123–144 (1984)
Rivest, R.L., Shapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993)
Sharygina, N., et al.: Dynamic Component Substitutability Analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 512–528. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Gheorghiu, M., Giannakopoulou, D., Păsăreanu, C.S. (2007). Refining Interface Alphabets for Compositional Verification. 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_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_23
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)