ABSTRACT
We are concerned with the problem of statically certifying (verifying) whether the client of a software component conforms to the component's constraints for correct usage. We show how conformance certification can be efficiently carried out in a staged fashion for certain classes of first-order safety (FOS) specifications, which can express relationship requirements among potentially unbounded collections of runtime objects. In the first stage of the certification process, we systematically derive an abstraction that is used to model the component state during analysis of arbitrary clients. In general, the derived abstraction will utilize first-order predicates, rather than the propositions often used by model checkers. In the second stage, the generated abstraction is incorporated into a static analysis engine to produce a certifier. In the final stage, the resulting certifier is applied to a client to conservatively determine whether the client violates the component's constraints. Unlike verification approaches that analyze a specification and client code together, our technique can take advantage of computationally-intensive symbolic techniques during the abstraction generation phase, without affecting the performance of client analysis. Using as a running example the Concurrent Modification Problem (CMP), which arises when certain classes defined by the Java Collections Framework are misused, we describe several different classes of certifiers with varying time/space/precision tradeoffs. Of particular note are precise, polynomial-time, flow- and context-sensitive certifiers for certain classes of FOS specifications and client programs. Finally, we evaluate a prototype implementation of a certifier for CMP on a variety of test programs. The results of the evaluation show that our approach, though conservative, yields very few "false alarms," with acceptable performance.
- T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 203--213, June 2001]] Google ScholarDigital Library
- T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001: SPIN Workshop, LNCS 2057, pages 103--122, 2001]] Google ScholarDigital Library
- J. Banning. An efficient way to find the side effects of procedure calls and the aliases of variables. In Proc. ACM Symp. on Principles of Programming Languages, pages 29--41, New York, NY, 1979. ACM Press]] Google ScholarDigital Library
- Canvas project. http://www.research.ibm.com/menage/canvas/]]Google Scholar
- P. Chan, R. Lee, and D. Kramer. The Java™ Class Libraries, Second Edition, Vol. 1, Supplement for the Java™ 2 Platform Standard Edition, v1.2, pages 296--325 Addison-Wesley, 1999]] Google ScholarDigital Library
- D. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 296--310, New York, NY, 1990. ACM Press]] Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. Computer Aided Verification, pages 154--169, 2000]] Google ScholarDigital Library
- K. D. Cooper and K. Kennedy. Interprocedural side-effect analysis in linear time. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 57--66, New York, NY, 1988. ACM Press]] Google ScholarDigital Library
- J. Corbett, M. Dwyer, J. Hatcliff, C. Pasareanu, Robby, S. Laubach, and H. Zheng. Bandera : Extracting finite-state models from Java source code. In Proc. 22nd Intl. Conf. on Software Engineering, pages 439--448, June 2000]] Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM Symp. on Principles of Programming Languages, pages 269--282, New York, NY, 1979. ACM Press]] Google ScholarDigital Library
- P. Cousot. Semantic foundations of program analysis. In S. Muchnick and N. Jones, editors, Program Flow Analysis: Theory and Applications, chapter~10, pages 303--342. Prentice-Hall, Englewood Cliffs, NJ, 1981]]Google Scholar
- J. Dean, D. Grove, and C. Chambers. Optimization of object-oriented programs using static class hierarchy analysis. Technical Report TR 94-12-01, Washington University, 1994. Also published in ECOOP'95 conference proceedings]] Google ScholarDigital Library
- R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 59--69, June 2001]] Google ScholarDigital Library
- E. W. Dijkstra. A Discipline of programing. Prentice-Hall, 1976]] Google ScholarDigital Library
- C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for ESC/Java. Technical Report 2000-003, Compaq Systems Research Center, 2000]]Google Scholar
- E. Gamma, R. Helm, R. Johnson, and J. Vlissides. Design Patterns. Addison-Wesley, Reading, MA, 1995]]Google ScholarDigital Library
- R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361--416, Mar. 2000]] Google ScholarDigital Library
- S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In In Proceedings of the 9th Conference on Computer-Aided Verification (CAV'97), pages 72--83, Haifa, Israel, June 1997]] Google ScholarDigital Library
- D. Jackson and A. Fekete. Lightweight analysis of object interactions. In Proc. Intl. Symp. on Theoretical Aspects of Computer Software, Sendai, Japan, October 2001]] Google ScholarDigital Library
- D. Jackson and M. Vaziri. Finding bugs with a constraint solver. In Proc. Intl. Symp. on Software Testing and Analysis, Portland, OR, August 2000]] Google ScholarDigital Library
- N. Jones and S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Proc. ACM Symp. on Principles of Programming Languages, pages 66--74, New York, NY, 1982. ACM Press]] Google ScholarDigital Library
- Kaffe. http://rpmfind.net/tools/Kaffe, 2001]]Google Scholar
- W. Landi and B. G. Ryder. Pointer-induced aliasing: A problem classification. In Proc. ACM Symp. on Principles of Programming Languages, pages 93--103, New York, NY, 1991. ACM Press]] Google ScholarDigital Library
- G. T. Leavens. The Java Modeling Language (JML). http://www.cs.iastate.edu/~leavens/JML.html]]Google Scholar
- K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC/Java user's manual. Technical Note 2000-002, Compaq Systems Research Center, October 2000]]Google Scholar
- T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In J. Palsberg, editor, Proc. Static Analysis Symp., volume 1824 of Lecture Notes in Computer Science, pages 280--301. Springer-Verlag, 2000]] Google ScholarDigital Library
- R. Muth and S. Debray. On the complexity of flow-sensitive dataflow analyses. In Proc. ACM Symp. on Principles of Programming Languages, pages 67--80, New York, NY, 2000. ACM Press]] Google ScholarDigital Library
- F. Nielson, H. R. Nielson, and C. Hankin. Principles of Program Analysis. Springer-Verlag, 2001]] Google ScholarDigital Library
- G. Ramalingam, A. Warshavsky, J. Field, and M. Sagiv. Deriving specialized heap analyses for verifying component-client conformance. Technical Report RC22145, IBM T.J. Watson Research Center, 2001]]Google Scholar
- T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proc. ACM Symp. on Principles of Programming Languages, pages 49--61, 1995]] Google ScholarDigital Library
- N. Rinetskey and M. Sagiv. Interprocedural shape analysis for recursive programs. In R. Wilhelm, editor, Proc. Intl. Conf. on Compiler Construction, volume 2027 of LNCS, pages 133--149. Springer-Verlag, 2001]] Google ScholarDigital Library
- N. Rinetzky. Interprocedural shape analysis. Master's thesis, Technion-Israel Institute of Technology, Haifa, Israel, Dec. 2000]]Google Scholar
- M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst., 20(1):1--50, Jan. 1998]] Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 105--118, 1999]] Google ScholarDigital Library
- H. Saïdi. Model checking guided abstraction and analysis. In J. Palsberg, editor, Proc. Static Analysis Symp., volume 1824 of Lecture Notes in Computer Science, pages 377--389. Springer-Verlag, 2000]] Google ScholarDigital Library
- R. Vallée-Rai, E. Gagnon, L.Hendren, P. Lam, P.Pominville, and V. Sundaresan. Optimizing Java bytecode using the Soot framework: Is it feasible? In Proc. Intl. Conf. on Compiler Construction, pages 18--34, Mar. 2000]] Google ScholarDigital Library
- E. Y.-B. Wang. Analysis of Recursive Types in an Imperative Language. PhD thesis, Univ. of Calif., Berkeley, CA, 1994]] Google ScholarDigital Library
- A. Warshavsky. http://www.math.tau.ac.il/~walex, 2001]]Google Scholar
- M. A. Weiss. Data Structures and Problem Solving Using Java. Addison-Wesley, second edition, 2001]] Google ScholarDigital Library
- E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 27--40, 2001]] Google ScholarDigital Library
Index Terms
- Deriving specialized program analyses for certifying component-client conformance
Recommendations
Deriving specialized program analyses for certifying component-client conformance
We are concerned with the problem of statically certifying (verifying) whether the client of a software component conforms to the component's constraints for correct usage. We show how conformance certification can be efficiently carried out in a staged ...
Formal Verification for C Program
Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. We present an approach for automatically verifying C programs against safety specifications based on finite state machine. The ...
Model Checking of Component Protocol Conformance -- Optimizations by Reducing False Negatives
In past years, a number of works considered behavioral protocols of components and discussed approaches for automatically checking of compatibality of protocols (protocol conformance) in component-based systems. The approaches are usually model-checking ...
Comments