Reasoning about Abstract Open Systems with Generalized Module Checking

  • Patrice Godefroid
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2855)


We present a framework for reasoning about abstract open systems. Open systems, also called “reactive systems” or “modules”, are systems that interact with their environment and whose behaviors depend on these interactions. Embedded software is a typical example of open system. Module checking [KV96] is a verification technique for checking whether an open system satisfies a temporal property no matter what its environment does. Module checking makes it possible to check adversarial properties of the “game” played by the open system with its environment (such as “is there a winning strategy for a malicious agent trying to intrude a secure system?”). We study how module checking can be extended to reason about 3-valued abstractions of open systems in such a way that both proofs and counter-examples obtained by verifying arbitrary properties on such abstractions are guaranteed to be sound, i.e., to carry over to the concrete system. We also introduce a new verification technique, called generalized module checking, that can improve the precision of module checking. The modeling framework and verification techniques developed in this paper can be used to represent and reason about abstractions automatically generated from a static analysis of an open program using abstraction techniques such as predicate abstraction. This application is illustrated with an example of open program and property that cannot be verified by current abstraction-based verification tools.


Model Check Temporal Logic Linear Temporal Logic Winning Strategy Atomic Proposition 
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. [AH01]
    de Alfaro, L., Henzinger, T.: Interface Automata. In: Proceedings of the 9th ACM Symposium on the Foundations of Software Engineering, FSE 2001 (2001)Google Scholar
  2. [AHKV98]
    Alur, R., Henzinger, T., Kupferman, O., Vardi, M.: Alternating Refinement Relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. [BG99]
    Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. [BG00]
    Bruns, G., Godefroid, P.: Generalized Model Checking: Reasoning about Partial State Spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. [BR01]
    Ball, T., Rajamani, S.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. [CDH+00]
    Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, H.Z., Zheng, V.: Bandera: Extracting Finite-State Models from Java Source Code. In: Proceedings of the 22nd International Conference on Software Engineering (2000)Google Scholar
  7. [Dam96]
    Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands (1996)Google Scholar
  8. [DD01]
    Das, S., Dill, D.L.: Successive Approximation of Abstract Transition Relations. In: Proceedings of 16th IEEE Symposium on Logic in Computer Science, LICS 2001, June 2001, pp. 51–58, Boston (2001)Google Scholar
  9. [Eme90]
    Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Elsevier/MIT Press, Amsterdam/ Cambridge (1990)Google Scholar
  10. [GHJ01]
    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)CrossRefGoogle Scholar
  11. [GJ02]
    Godefroid, P., Jagadeesan, R.: Automatic Abstraction Using Generalized Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. [GJ03]
    Godefroid, P., Jagadeesan, R.: On the Expressiveness of 3-Valued Models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206–222. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  13. [GS97]
    Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  14. [HJMS02]
    Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, Portland, January 2002, pp. 58–70 (2002)Google Scholar
  15. [HJS01]
    Huth, M., Jagadeesan, R., Schmidt, D.: Modal Transition Systems: a Foundation for Three-Valued Program Analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, p. 155. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  16. [Kle87]
    Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1987)Google Scholar
  17. [Koz83]
    Kozen, D.: Results on the Propositional Mu-Calculus. Theoretical Computer Science 27, 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  18. [KV96]
    Kupferman, O., Vardi, M.: Module Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 75–86. Springer, Heidelberg (1996)Google Scholar
  19. [LT88]
    Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: Proceedings of Third Annual Symposium on Logic in Computer Science, pp. 203–210. IEEE Computer Society Press, Los Alamitos (1988)CrossRefGoogle Scholar
  20. [VHBP00]
    Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proceedings of 15th International Conference on Automated Software Engineering, ASE 2000, Grenoble (September 2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Patrice Godefroid
    • 1
  1. 1.Bell LaboratoriesLucent Technologies 

Personalised recommendations