Abstract
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.
Chapter PDF
References
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)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient Detection of Vacuity in Temporal Model Checking. FMSD 18(2), 141–163 (2001)
Belnap, N.D.: A Useful Four-Valued Logic. In: Dunn, J., Epstein, G. (eds.) Modern Uses of Multiple-Valued Logic, pp. 30–56 (1977)
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)
Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM TOSEM 12(4), 1–38 (2003)
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)
Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient Debugging in a Formal Verification Environment. STTT 4(3), 335–348 (2003)
Dwyer, M., Avrunin, G., Corbett, J.: Patterns in Property Specifications for Finite-State Verification. In: Proceedings of ICSE’99 (May 1999)
Giannakopoulou, D., Pasareanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: Proceedings of ASE’02, pp. 3–12 (2002)
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)
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)
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)
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)
Heimdahl, M., Leveson, N.: Completeness and Consistency in Hierarchical State-Based Requirements. IEEE TSE 22(6), 363–377 (1996)
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)
Kupferman, O., Vardi, M.: Vacuity Detection in Temporal Model Checking. STTT 4(2), 224–233 (2003)
Kupferman, O., Vardi, M.Y., Wolper, P.: “Module Checking”. Information and Computation 164(2), 322–344 (2001)
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)
Lygeros, J., Lynch, N.: On the Formal Verification of the TCAS Conflict Resolution Algorithms. In: Proceedings of Conf. on Decision and Control (December 1997)
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)
Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging Overconstrained Declarative Models Using Unsatisfiable Cores. In: Proceedings of ASE’03 (2003)
US Dept. of Transportation: Introduction to TCAS II. FAA (March 1990)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Chechik, M., Gheorghiu, M., Gurfinkel, A. (2007). Finding Environment Guarantees. In: Dwyer, M.B., Lopes, A. (eds) Fundamental Approaches to Software Engineering. FASE 2007. Lecture Notes in Computer Science, vol 4422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71289-3_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-71289-3_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71288-6
Online ISBN: 978-3-540-71289-3
eBook Packages: Computer ScienceComputer Science (R0)