Abstract
We present a new technique for automatically synthesizing the assumptions needed in compositional model checking. The compositional approach reduces the proof that a property is satisfied by the parallel composition of two processes to the simpler argument that the property is guaranteed by one process provided that the other process satisfies an assumption A. Finding A manually is a difficult task that requires detailed insight into how the processes cooperate to satisfy the property. Previous methods to construct A automatically were based on the learning algorithm L *, which represents A as a deterministic automaton and therefore has exponential worst-case complexity. Our new technique instead represents A as an equivalence relation on the states, which allows for a quasi-linear construction. The model checker can therefore apply compositional reasoning without risking an exponential penalty for computing A.
This work was partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS).
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
Alur, R., Cerny, P., Madhusudan, P., Nam, W.: Synthesis of interface specifications for Java classes. In: Proc. POPL, pp. 98–109. ACM Press, New York (2005)
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)
Cheung, S.C., Kramer, J.: Context constraints for compositional reachability analysis. ACM Trans. Softw. Eng. Methodol. 5(4), 334–377 (1996)
Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proc. LICS, pp. 353–362 (1989)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: 19th ACM Symp. Princ. of Prog. Lang., pp. 343–354 (1992)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, 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 Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: Uncertainty, but with precision. In: Proc. LICS, pp. 170–179 (2004)
Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Assumption generation for software component verification. In: Proc. ASE, pp. 3–12. IEEE Computer Society, Los Alamitos (2002)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)
Graf, S., Steffen, B., Lüttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects of Computation 8 (September 1996)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)
Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: Methodology and case studies. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998)
Holzmann, G.J.: The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Proc. European Symposium on Programming, pp. 155–169. Springer, Heidelberg (2001)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407. Springer, Heidelberg (1990)
Larsen, K.G., Thomsen, B.: A modal process logic. In: Proc. LICS, pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)
Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001)
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)
Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and models of concurrent systems, pp. 123–144. Springer, Heidelberg (1985)
Sabnani, K.K., Lapone, A.M., Ümit Uyar, M.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940–948 (1989)
Tai, K.-C., Koppol, P.V.: An incremental approach to reachability analysis of distributed programs. In: Proc. IWSSD, pp. 141–150. IEEE Computer Society Press, Los Alamitos (1993)
Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing 9(2), 149–174 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Finkbeiner, B., Schewe, S., Brill, M. (2006). Automatic Synthesis of Assumptions for Compositional Model Checking. In: Najm, E., Pradat-Peyre, JF., Donzeau-Gouge, V.V. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2006. FORTE 2006. Lecture Notes in Computer Science, vol 4229. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11888116_12
Download citation
DOI: https://doi.org/10.1007/11888116_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-46219-4
Online ISBN: 978-3-540-46220-0
eBook Packages: Computer ScienceComputer Science (R0)