Reasoning about Abstract Open Systems with Generalized Module Checking
- 450 Downloads
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.
KeywordsModel Check Temporal Logic Linear Temporal Logic Winning Strategy Atomic Proposition
Unable to display preview. Download preview PDF.
- [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
- [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
- [Dam96]Dams, D.: Abstract interpretation and partition refinement for model checking. PhD thesis, Technische Universiteit Eindhoven, The Netherlands (1996)Google Scholar
- [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
- [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
- [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
- [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
- [Kle87]Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1987)Google Scholar
- [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
- [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