Abstract
Compositional verification is based on the idea that the correctness check of a complex system can be divided into smaller verification tasks for its components. In this paper, we show how to decompose a specification into components when either no such decomposition is given, or when the given composition does not lend itself to an efficient compositional verification. Our decomposition is the starting point for an application of the L* learning algorithm, generating assumptions for an assume-guarantee reasoning. We prove correctness of the decomposition as well as present experimental results using the model checker FDR2 as the teacher during learning.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75, 87–106 (1987)
Barringer, H., Giannakopoulou, D., Pasareanu, C.S.: Proof rules for automated compositional verification through learning. In: International Workshop on Specification and Verification of Component Based Systems, Finland (2003)
Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison (1987)
Brückner, I.: Slicing Integrated Formal Specifications for Verification. PhD thesis, Universität Paderborn (2008)
Brückner, I., Wehrheim, H.: Slicing an integrated formal method for verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 360–374. Springer, Heidelberg (2005)
Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an investigation of decomposition for assume-guarantee reasoning. In: ISSTA 2006: Proceedings of the 2006 international symposium on Software testing and analysis, pp. 97–108. ACM Press, New York (2006)
Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
de Roever, W.P., Hanneman, U., Hooiman, J., Lakhneche, Y., Poel, M., Zwiers, J., de Boer, F.: Concurrency Verification. Cambridge University Press, Cambridge (2001)
Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)
Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS 1997), vol. 2, pp. 423–438. Chapman and Hall, Boca Raton (1997)
Fischer, C., Wehrheim, H.: Model-checking CSP-OZ specifications with FDR. In: IFM, pp. 315–334 (1999)
Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informatica 9(2) (1978)
Gallagher, K.B., Lyle, J.R.: Using program slicing in software maintenance. IEEE Transactions on Software Engineering 17(8), 751–761 (1991)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Jones, C.B.: Tentative steps towards a development method for interfering programs. Transactions on Programming Languages and Systems 5(4), 596–619 (1983)
Formal Systems (Europe) Ltd. Failure divergence refinement: Fdr2 user manual (1997)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417–426 (1981)
Nam, W., Alur, R.: 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)
Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 139–153. Springer, Heidelberg (2000)
Reps, T.W., Rosay, G.: Precise interprocedural chopping. In: SIGSOFT FSE, pp. 41–52 (1995)
Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)
Schneider, S., Treharne, H.: Verifying controlled components. In: IFM, pp. 87–107 (2004)
Smith, G.: The Object-Z Specification Language. Kluwer Academic Publishers, Dordrecht (2000)
Tip, F.: A survey of program slicing techniques. Journal of Programming Languages 3, 121–189 (1995)
Tonella, P.: Using a concept lattice of decomposition slices for program understanding and impact analysis. IEEE Trans. Software Eng. 29(6), 495–509 (2003)
Weiser, M.: Programmers use slices when debugging. Commun. ACM 25(7), 446–452 (1982)
Wonisch, D.: Automatisiertes kompositionelles Model Checking von CSP Spezifikationen. Bachelor’s thesis, Universität Paderborn (April 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Metzler, B., Wehrheim, H., Wonisch, D. (2008). Decomposition for Compositional Verification. In: Liu, S., Maibaum, T., Araki, K. (eds) Formal Methods and Software Engineering. ICFEM 2008. Lecture Notes in Computer Science, vol 5256. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88194-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-88194-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88193-3
Online ISBN: 978-3-540-88194-0
eBook Packages: Computer ScienceComputer Science (R0)