Compositional Verification for Component-Based Systems and Application

  • Saddek Bensalem
  • Marius Bozga
  • Joseph Sifakis
  • Thanh-Hung Nguyen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)


We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants which are over-approximations of components’ reachability sets. Interaction invariants which are constraints on the states of components involved in interactions. Interaction invariants are obtained by computing traps of finite-state abstractions of the verified system. The method is applied for deadlock verification in the D-Finder tool. D-Finder is an interactive tool that takes as input BIP programs and applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants. The experimental results on non-trivial examples allow either to prove deadlock-freedom or to identify very few deadlock configurations that can be analyzed by using state space exploration.


Parallel Composition Temperature Control System Atomic Component State Predicate Component Invariant 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Kupferman, O., Vardi, M.Y.: Modular model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 381–401. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.: Reactive modules. In: Proceedings of the 11th Annual Symposium on LICS, pp. 207–218. IEEE Computer Society Press, Los Alamitos (1996)Google Scholar
  3. 3.
    Abadi, M., Lamport, L.: Conjoining specification. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)CrossRefGoogle Scholar
  4. 4.
    Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th Annual Symposium on LICS, pp. 353–362. IEEE Computer Society Press, Los Alamitos (1989)Google Scholar
  5. 5.
    Chandy, K., Misra, J.: Parallel program design: a foundation. Addison-Wesley Publishing Company, Reading (1988)zbMATHGoogle Scholar
  6. 6.
    Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)CrossRefGoogle Scholar
  7. 7.
    McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 24–35. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  8. 8.
    Pnueli, A.: In transition from global to modular temporal reasoning about programs, 123–144 (1985)Google Scholar
  9. 9.
    Stark, E.W.: A proof technique for rely/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol. 206, pp. 369–391. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  10. 10.
    Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM Transactions on Software Engineering and Methodology 17(2) (2008)Google Scholar
  11. 11.
    Peterson, J.: Petri Net theory and the modelling of systems. Prentice-Hall, Englewood Cliffs (1981)zbMATHGoogle Scholar
  12. 12.
    Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2(3), 359–385 (1980)CrossRefzbMATHGoogle Scholar
  13. 13.
    Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: SEFM, pp. 3–12 (2006)Google Scholar
  14. 14.
    Team, O.: The omega library. Version 1.1.0 (November 1996)Google Scholar
  15. 15.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS 138(1), 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173–180 (2007)Google Scholar
  19. 19.
    Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. FMSD 15(1), 75–92 (1999)Google Scholar
  20. 20.
    Sifakis, J.: Structural properties of petri nets. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 474–483. Springer, Heidelberg (1978)CrossRefGoogle Scholar
  21. 21.
    Yamauchi, M., Watanabe, T.: Time complexity analysis of the minimal siphon extraction problem of petri nets. IEICE Transactions on Communications/Electronics/Information and Systems (1999)Google Scholar
  22. 22.
    Tanimoto, S., Yamauchi, M., Watanabe, T.: Finding minimal siphons in general petri nets. IEICE Trans. on Fundamentals in Electronics, Communications and Computer Science E79-A(11), 1817–1824 (1996)Google Scholar
  23. 23.
    Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems automatically and compositionally. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 319–331. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  24. 24.
    Bensalem, S., Lakhnech, Y., Owre, S.: Invest: A tool for the verification of invariants. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 505–510. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Saddek Bensalem
    • 1
  • Marius Bozga
    • 1
  • Joseph Sifakis
    • 1
  • Thanh-Hung Nguyen
    • 1
  1. 1.Verimag LaboratoryUniversité Joseph Fourier Grenoble, CNRSFrance

Personalised recommendations