Finding Environment Guarantees

  • Marsha Chechik
  • Mihaela Gheorghiu
  • Arie Gurfinkel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4422)


When model checking a software component, a model of the environment in which that component is supposed to run is constructed. One of the major threats to the validity of this kind of analysis is the correctness of the environment model. In this paper, we identify and formalize a problem related to environment models — environment guarantees. It captures those cases where the correctness of the component under analysis is due solely to the model of its environment. Environment guarantees provides a model-based analog to a property-based notion of vacuity by identifying cases when the component is irrelevant to satisfaction of a property. The paper also presents a model checking technique for the detection of environment guarantees. We show the effectiveness of our technique by applying it to a previously published study of TCAS II, where it finds a number of environment guarantees.


Model Check Temporal Logic Environment Model Kripke Structure Boolean State 
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.


  1. 1.
    Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Y. Vardi, M.: Enhanced Vacuity Detection in Linear Temporal Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368–380. Springer, Heidelberg (2003)Google Scholar
  2. 2.
    Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient Detection of Vacuity in Temporal Model Checking. FMSD 18(2), 141–163 (2001)zbMATHGoogle Scholar
  3. 3.
    Belnap, N.D.: A Useful Four-Valued Logic. In: Dunn, J., Epstein, G. (eds.) Modern Uses of Multiple-Valued Logic, pp. 30–56 (1977)Google Scholar
  4. 4.
    Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D.: Model Checking Large Software Specifications. IEEE TSE 24(7), 498–520 (1998)Google Scholar
  5. 5.
    Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM TOSEM 12(4), 1–38 (2003)CrossRefGoogle Scholar
  6. 6.
    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient Debugging in a Formal Verification Environment. STTT 4(3), 335–348 (2003)Google Scholar
  8. 8.
    Dwyer, M., Avrunin, G., Corbett, J.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of ICSE’99 (May 1999)Google Scholar
  9. 9.
    Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: Proceedings of ASE’02, pp. 3–12 (2002)Google Scholar
  10. 10.
    Godefroid, P.: Reasoning about Abstract Open Systems with Generalized Module Checking. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 223–240. Springer, Heidelberg (2003)Google Scholar
  11. 11.
    Grumberg, O., Long, D.E.: Model Checking and Modular Verification. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, Springer, Heidelberg (1991)Google Scholar
  12. 12.
    Gurfinkel, A., Chechik, M.: Multi-valued Model Checking via Classical Model Checking. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266–280. Springer, Heidelberg (2003)Google Scholar
  13. 13.
    Gurfinkel, A., Chechik, M.: Extending Extended Vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 306–321. Springer, Heidelberg (2004)Google Scholar
  14. 14.
    Heimdahl, M., Leveson, N.: Completeness and Consistency in Hierarchical State-Based Requirements. IEEE TSE 22(6), 363–377 (1996)Google Scholar
  15. 15.
    Kupferman, O., Vardi, M.Y.: Robust Satisfaction. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 383–398. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. 16.
    Kupferman, O., Vardi, M.: Vacuity Detection in Temporal Model Checking. STTT 4(2), 224–233 (2003)Google Scholar
  17. 17.
    Kupferman, O., Vardi, M.Y., Wolper, P.: “Module Checking”. Information and Computation 164(2), 322–344 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Leveson, N.G., Heimdahl, M.P.E., Hildreth, H., Reese, J.D.: Requirements Specification for Process-Control Systems. IEEE TSE 20(9), 684–707 (1994)Google Scholar
  19. 19.
    Lygeros, J., Lynch, N.: On the Formal Verification of the TCAS Conflict Resolution Algorithms. In: Proceedings of Conf. on Decision and Control (December 1997)Google Scholar
  20. 20.
    Purandare, M., Somenzi, F.: Vacuum Cleaning CTL Formulae. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 485–499. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging Overconstrained Declarative Models Using Unsatisfiable Cores. In: Proceedings of ASE’03 (2003)Google Scholar
  22. 22.
    US Dept. of Transportation: Introduction to TCAS II. FAA (March 1990)Google Scholar

Copyright information

© Springer Berlin Heidelberg 2007

Authors and Affiliations

  • Marsha Chechik
    • 1
  • Mihaela Gheorghiu
    • 1
  • Arie Gurfinkel
    • 1
  1. 1.University of Toronto, Toronto, ON M5S 3G4Canada

Personalised recommendations