This paper addresses the formal verification of distributed systems comprising a dynamically changing and potentially unbounded number of processes. We employ the spotlight principle to obtain a concise finitary abstraction of the system and devise an abstraction refinement strategy guided by the analysis of abstract counterexamples.

It turns out that the key problem for spotlight refinement is the identification of spurious counterexamples. We observe that the problem is in general undecidable, and provide a sound but incomplete method that is able to solve the problem for many practically relevant systems. Our method is driven by a three-valued satisfaction relation for temporal specifications that accounts for the fact that concrete counterexamples can be identified in the abstracted system if they occur within the spotlight.


  1. 1.
    UNISIG: Subset 026-ch. 3; vers. 2.2.2 (srs) (March 2002),
  2. 2.
    Kripke, S.: Semantical Considerations on Modal Logic. Acta Phil. Fennica 16, 83–94 (1963)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  4. 4.
    Kesten, Y., Pnueli, A.: Control and Data Abstraction: The Cornerstones of Practical Formal Verification. International Journal on Software Tools for Technology Transfer 2(4), 328–342 (2000)CrossRefzbMATHGoogle Scholar
  5. 5.
    Fitting, M., Mendelsohn, R.L.: First Order Modal Logic. Kluwer, Dordrecht (1998)CrossRefzbMATHGoogle Scholar
  6. 6.
    Brayton, R.K., Hachtel, G.D., Sangiovanni - Vincentelli, A.L., Somenzi, F., Aziz, A., Cheng, S.T., Edwards, S.A., Khatri, S.P., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 428–432. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  7. 7.
    Holzmann, G.J.: The SPIN model checker: Primer and reference manual. Addison-Wesley, Reading (2004)Google Scholar
  8. 8.
    Wachter, B., Westphal, B.: The Spotlight Principle. On Combining Process-Summarising State Abstractions. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 182–198. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  10. 10.
    Rakow, J.: Verification of Dynamic Communication Systems. Master’s thesis, Carl von Ossietzky Universität Oldenburg (April 2006)Google Scholar
  11. 11.
    Westphal, B.: LSC Verification for UML Models with Unbounded Creation and Destruction. Electr. Notes Theor. Comput. Sci. 144(3), 133–145 (2006)CrossRefGoogle Scholar
  12. 12.
    Miller, A., Calder, M.: An automatic abstraction technique for verifying featured, parameterised systems. Theor. Comput. Sci. (to appear, 2007)Google Scholar
  13. 13.
    Damm, W., Westphal, B.: Live and let die: LSC-based verification of UML-models. Science of Computer Programming 55(1–3), 117–159 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Toben, T.: Non-Interference Properties for Data-Type Reduction of Communicating Systems. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 619–638. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Bauer, J., Toben, T., Westphal, B.: Mind the Shapes: Abstraction Refinement via Topology Invariants. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 35–50. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Bauer, J., Wilhelm, R.: Static Analysis of Dynamic Communication Systems by Partner Abstraction. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 249–264. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    König, B., Kozioura, V.: Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)Google Scholar
  18. 18.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)CrossRefGoogle Scholar
  19. 19.
    Kleene, S.C.: Introduction to metamathematics. Bibl. Matematica. North-Holland, Amsterdam (1952)zbMATHGoogle Scholar
  20. 20.
    Toben, T.: Spotlight Abstraction Refinement by Evolution Constraints. PhD thesis, Carl von Ossietzky Universität Oldenburg (to appear, 2008)Google Scholar
  21. 21.
    Pnueli, A.: The temporal logic of programs. In: Proc. FOCS, pp. 46–57. IEEE, Los Alamitos (1977)Google Scholar
  22. 22.
    Westphal, B.: Specification and Verification of Dynamic Topology Systems. PhD thesis, Carl von Ossietzky Universität Oldenburg (2008)Google Scholar
  23. 23.
    Xie, F., Browne, J.C.: Integrated State Space Reduction for Model Checking Executable Object-oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, pp. 64–79. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  24. 24.
    Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: Proc. LICS 1986, pp. 332–344. IEEE Computer Society, Los Alamitos (1986)Google Scholar
  25. 25.
    Westphal, B., Cook, B.S.: LSC Verification for UML Models with Unbounded Creation and Destruction. In: B. Cook, S., Stoller, W.V. (eds.) Proc. SoftMC 2005. ENTCS, vol. 144(3), pp. 133–145. Elsevier B.V, Amsterdam (2005)Google Scholar
  26. 26.
    Haartsen, J.: Bluetooth – the universal radio interface for adhoc, wireless connectivity. Ericsson Review 3 (1998)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Tobe Toben
    • 1
  1. 1.Carl von Ossietzky Universität OldenburgGermany

Personalised recommendations