Abstract
Model checking techniques have proven effective for checking a number of non-trivial concurrent object-oriented software systems. However, due to the high computational and memory costs, a variety of model reduction techniques are needed to overcome current limitations on applicability and scalability. Conventional wisdom holds that static program slicing can be an effective model reduction technique, yet anecdotal evidence is mixed, and there has been no work that has systematically studied the costs/benefits of slicing for model reduction in the context of model checking source code for realistic systems.
In this paper, we present an overview of the sophisticated Indus program slicer that is capable of handling full Java and is readily applicable to interesting off-the-shelf concurrent Java programs. Using the Indus program slicer as part of the next generation of the Bandera model checking framework, we experimentally demonstrate significant benefits from using slicing as a fully automatic model reduction technique. Our experimental results consider a number of Java systems with varying structural properties, the effects of combining slicing with other well-known model reduction techniques such as partial order reductions, and the effects of slicing for different classes of properties. Our conclusions are that slicing concurrent object-oriented source code provides significant reductions that are orthogonal to a number of other reduction techniques, and that slicing should always be applied due to its automation and low computational costs.
Chapter PDF
References
Andrews, G.R.: Concurrent Programming: Principles and Practice. Addison-Wesley, Reading (1991)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic predicate abstraction of C programs. In: Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI 2001), June 2001, pp. 203–213 (2001)
Bandera. SAnToS Laboratory, http://bandera.projects.cis.ksu.edu
Bozga, M., Fernandez, J.-C., Ghirvu, L., Graf, S., Krimm, J.-P., Mounier, L.: IF: A validation environment for timed asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 543–547. Springer, Heidelberg (2000)
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder – A second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)
Clarke, E., Fujita, M., Rajan, S.P., Reps, T., Shankar, S., Teitelbaum, T.: Program slicing of hardware description languages. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 298–313. Springer, Heidelberg (1999)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Engeler, E. (ed.) Logic of Programs 1979. LNCS, vol. 125, pp. 52–71. Springer, Heidelberg (1981)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Păsăreanu, C.S., Robby, Zheng, H.: Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In: Proceedings of the 22nd International Conference on Software Engineering (June 2000)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Robby: Expressing checkable properties of dynamic systems: The Bandera Specification Language. International Journal on Software Tools for Technology Transfer (2002)
Do, H., Elbaum, S., Rothermel, G.: Infrastructure support for controlled experimentation with software testing and regression testing techniques. In: 2004 International Symposium on Empirical Software Engineering (ISESE 2004), pp. 60–70. IEEE Computer Society Press, Los Alamitos (2004)
Dwyer, M.B., Hatcliff, J., Joehanes, R., Laubach, S., P˘as˘areanu, C.S., Păsăreanu, C.S., Robby, Visser, W., Zheng, H.: Tool-supported program abstraction for finite-state verification. In: Proceedings of the 23rd International Conference on Software Engineering (May 2001)
Dwyer, M.B., Hatcliff, J., Prasad, V.R., Robby: Exploiting object escape and locking information in partial order reductions for concurrent object-oriented programs. Formal Methods in System Designs 25(2–3), 199–240 (2004)
Eclipse Consortium. Eclipse website, http://www.eclipse.org
Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, Long Beach, California, USA, January 2005, pp. 110–121. ACM, New York (2005)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
Groce, A., Visser, W.: Model checking Java programs using structural heuristics. In: Proceedings of the International Symposium on Software Testing and Analysis, pp. 12–21. ACM Press, New York (2002)
Hatcliff, J., Corbett, J., Dwyer, M.B., Sokolowski, S., Zheng, H.: A formal study of slicing for multi-threaded programs with JVM concurrency primitives. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, p. 1. Springer, Heidelberg (1999)
Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Journal of Higher-order and Symbolic Computation 13(4), 315–353 (2000)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–294 (1997)
Holzmann, G.J.: Personal communication (October 2005)
Iosif, R.: Symmetry Reduction Criteria for Software Model Checking. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 22–41. Springer, Heidelberg (2002)
Java Grande Benchmarking Project. Java Grande forum benchmark suite – thread version 1.0., http://www.epcc.ed.ac.uk/computing/researchactivities/javagrande/
Jayaraman, G., Ranganath, V.P., Hatcliff, J.: Kaveri: Delivering the Indus Java Program Slicer to Eclipse. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 269–272. Springer, Heidelberg (2005)
Jia, G., Graf, S.: Verification experiments on the MASCARA protocol. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 123–142. Springer, Heidelberg (2001)
Krinke, J.: Static slicing of threaded programs. In: Proceedings ACM SIGPLAN/SIGFSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 1998), June 1998. ACM SIGPLAN Notices, vol. 33(7), pp. 35–42. ACM Press, New York (1998)
Millett, L.I., Teitelbaum, T.: Slicing Promela and its applications to model checking, simulation, and protocol understanding. In: Proceedings of the 4th International SPIN Workshop. LNCS (1998)
Nanda, M.G., Ramesh, S.: Slicing concurrent programs. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA 2000), pp. 180–190 (2000)
Podgurski, A., Clarke, L.: A formal model of program dependences and its implications for software testing, debugging, and maintenance. IEEE Transactions on Software Engineering 16(8), 965–979 (1990)
Ranganath, V.P.: Indus, http://indus.projects.cis.ksu.edu
Ranganath, V.P.: Object-flow analysis for optimizing finite-state models of Java software. Master’s thesis, Kansas State University (2002)
Ranganath, V.P., Amtoft, T., Banerjee, A., Dwyer, M.B., Hatcliff, J.: A new foundation for control-dependence and slicing for modern program structures. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 77–93. Springer, Heidelberg (2005)
Ranganath, V.P., Hatcliff, J.: Pruning interference and ready dependences for slicing concurrent Java programs. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 39–56. Springer, Heidelberg (2004)
Robby, Dwyer, M.B., Hatcliff, J.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference / 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering (2003)
Robby, Dwyer, M.B., Hatcliff, J., Iosif, R.: Space-reduction strategies for model checking dynamic systems. In: Proceedings of the 2003 Workshop on Software Model Checking (July 2003)
Sen, A., Bhadra, J., Garg, V.K., Abraham, J.A.: Formal verification of a system-on-chip using computation slicing. In: International Test Conference ITC, October 2004, pp. 810–819 (2004)
Stoller, S.: Model-checking multi-threaded distributed Java programs. International Journal on Software Tools for Technology Transfer (2002)
Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A Java bytecode checker based on Moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 541–545. Springer, Heidelberg (2005)
Tip, F.: A survey of program slicing techniques. Journal of programming languages 3, 121–189 (1995)
Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot – A Java optimization framework. In: Proceedings of CASCON 1999 (November 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V., Robby, Wallentine, T. (2006). Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_5
Download citation
DOI: https://doi.org/10.1007/11691372_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)