×

Translating Java for multiple model checkers: The Bandera back-end. (English) Zbl 1086.68557

Summary: One approach to model checking program source code is to view a model checker as a target machine. In this setting, program source code is translated to a model checker’s input language using a process that shares much in common with program compilation. For example, well-defined intermediate program representations are used to stage the translation through a series of analyses and optimizing transformations and target-specific details are isolated in code generation modules.
In this paper, we present the Bandera Intermediate Representation (BIR) – a guarded-assignment transformation system language that has been designed to support the translation of Java programs to a variety of model checkers. BIR includes constructs, such as inheritance, dynamic creation of data, and locking primitives, that are designed to model the semantics of Java primitives. BIR also includes several non-deterministic choice constructs that support abstraction in modeling and specification of properties of dynamic heap structures.
We have developed a BIR-based tool infrastructure that has been applied to develop customized analysis frameworks for several different input languages using different model checking tools. We present BIR’s type system and operational semantics in sufficient detail to support similar applications by other researchers. This semantics details several state space reductions and state space search variations. We describe the translation of Java to BIR and how BIR is translated to the input languages of several model checkers.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI HAL

References:

[1] R. Alur, R. Grosu, and M. McDougall, ”Efficient reachability analysis of hierarchical reactive machines,” in Proceedings 12th International Conference on Computer Aided Verification, 2000. · Zbl 0974.68551
[2] E. Ashcroft and Z. Manna, ”Formalization of properties of parallel programs,” Machine Intelligence, pp. 17–41, 1972. · Zbl 0263.68016
[3] George S. Avrunin, James C. Corbett, and Matthew B. Dwyer, ”Benchmarking finite-state verifiers,” International Journal on Software Tools for Technology Transfer, Vol. 2, No. 4, pp. 317–320, 2000.
[4] T. Ball and S. Rajamani, ”Bebop: A symbolic model-checker for boolean programs,” in K. Havelund, John Penix, and Willem Visser (Eds.), Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 113–130. · Zbl 0976.68540
[5] Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, Cesar Mu noz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Saïdi, N. Shankar, Eli Singerman, and Ashish Tiwari, ”An overview of SAL,” in Proceedings of the Fifth Langley Formal Methods Workshop, June 2000.
[6] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, ”NuSMV : A new symbolic model checker,” International Journal on Software Tools for Technology Transfer, Vol. 2, No. 4, pp. 410–425, 2000. · Zbl 1059.68582
[7] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella, ”Nusmv 2: An opensource tool for symbolic model checking,” in Proceeding of International Conference on Computer-Aided Verification (CAV), 2002. · Zbl 1010.68766
[8] E.M. Clarke and E.A. Emerson, ”Synthesis of synchronization skeletons for branching time temporal logic,” Lecture Notes in Computer Science, Vol. 131, 1981. · Zbl 0546.68014
[9] James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Păsăreanu, Robby, and Hongjun Zheng, ”Bandera: Extracting finite-state models from Java source code,” in Proceedings of the 22nd International Conference on Software Engineering, June 2000.
[10] James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby, ”Bandera: A source-level interface for model checking Java programs,” in Proceedings of the 22nd International Conference on Software Engineering, June 2000. · Zbl 0976.68536
[11] James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby, ”Expressing checkable properties of dynamic systems: The bandera specification language,” International Journal on Software Tools for Technology Transfer, Vol. 4, No. 1, 2002. · Zbl 0976.68536
[12] Jeffrey Dean, David Grove, and Craig Chambers, ”Optimization of object-oriented programs using static class hierarchy analysis,” Lecture Notes in Computer Science, Vol. 952, 1995.
[13] C. Demartini, R. Iosif, and R. Sisto, ”A deadlock detection tool for concurrent Java programs,” Software - Practice and Experience, Vol. 29, No. 7, pp. 577–603, 1999. · Zbl 05467802
[14] C. Demartini, R. Iosif, and R. Sisto, ”dSPIN: A dynamic extension of SPIN,” in Theoretical and Applied Aspects of SPIN Model Checking (LNCS 1680), September 1999.
[15] Xianghua Deng, Matthew B. Dwyer, John Hatcliff, and Masaaki Mizuno, ”invariant-based specification, synthesis, and verification of synchronization in concurrent programs,” in Proceedings of the 24nd International Conference on Software Engineering, May 2002. · Zbl 1126.68472
[16] Matthew Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina Pasareanu, Robby, Willem Visser, and Hongjun Zheng, ”Tool-supported program abstraction for finite-state verification,” in Proceedings of the 23rd International Conference on Software Engineering, 2001, pp. 177–187.
[17] Matthew B. Dwyer, John Hatcliff, Roby Joehanes, Shawn Laubach, Corina S. Păsăreanu, Robby, Willem Visser, and Hongjun Zheng, ”Tool-supported program abstraction for finite-state verification,” in Proceedings of the 23rd International Conference on Software Engineering, May 2001.
[18] M.B. Dwyer, G.S. Avrunin, and J.C. Corbett, ”Patterns in property specifications for finite-state verification,” in Proceedings of the 21st International Conference on Software Engineering, May 1999.
[19] Stefan Edelkamp, Alberto Lluch-Lafuente, and Stefan Leue, ”Directed model-checking with HSF-Spin,” in Proceedings of the 8th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, 2001. · Zbl 0986.68521
[20] R. Gerth, R. Kuiper, D. Peled, and W. Penczek, ”A partial order approach to branching time logic model checking,” in Proceedings 3rd Israel Symposium on Theory on Computing and Systems, 1995, pp. 130–139. · Zbl 1045.68588
[21] Carlo Ghezzi and Mehdi Jazayeri, ”Programming Language Concepts 3rd edition,” John Wiley and Sons, 1997. · Zbl 0584.68012
[22] R.J. van Glabbeek and W.P. Weijland, ”Branching time and abstraction in bisimulation semantics,” Journal of the ACM, Vol. 43, No. 3, pp. 555–600, 1996. · Zbl 0882.68085
[23] Patrice Godefroid, ”Partial-order methods for the verification of concurrent systems,” Lecture Notes in Computer Science, Vol. 1032, 1996. · Zbl 1293.68005
[24] Patrice Godefroid, ”Model-checking for programming languages using VeriSoft,” in Proceedings of the 24th ACM Symposium on Principles of Programming Languages (POPL’97), January 1997, pp. 174–186,
[25] John Hatcliff, James C. Corbett, Matthew B. Dwyer, Stefan Sokolowski, and Hongjun Zheng, ”A formal study of slicing for multi-threaded programs with JVM concurrency primitives,” in Proceedings of the 6th International Static Analysis Symposium (SAS’99), September 1999.
[26] John Hatcliff, Matthew B. Dwyer, Corina S. Păsăreanu, and Robby, ”Foundations of the bandera abstraction tools,” in The Essence of Computation, LNCS 1490, 2000. · Zbl 1026.68511
[27] John Hatcliff, Matthew B. Dwyer, and Hongjun Zheng, ”Slicing software for model construction,” Higher-order and Symbolic Computation, Vol. 13, No. 4, 2000. · Zbl 0972.68021
[28] K. Havelund and T. Pressburger, ”Model checking Java programs using Java PathFinder,” International Journal on Software Tools for Technology Transfer, 1999. · Zbl 1059.68585
[29] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre, ”Lazy abstraction,” in Proceedings of the ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, Portland, Oregon, January 2002. · Zbl 1323.68374
[30] Gerard Holzmann, ”The spin model checker,” IEEE Transactions on Software Engineering, Vol. 23, pp. 279–295, 1997. · Zbl 05113845
[31] Gerard Holzmann and Doron Peled, ”An improvement in formal verification,” Formal Description Techniques, pp. 197–211, 1994.
[32] Gerard J. Holzmann, ”The model checker SPIN,” IEEE Transactions on Software Engineering, Vol. 23, No. 5, pp. 279–294, 1997. · Zbl 05113845
[33] Gerard J. Holzmann and Margaret H. Smith, ”Software model checking: Extracting verification models from source code,” in Proceedings of FORTE/PSTV’99, November 1999.
[34] Radu Iosif, ”Exploiting heap symmetries in explicit-state model checking of software,” in Proc 16th IEEE International Conference on Automated Software Engineering, 2001, pp. 254–261.
[35] Radu Iosif and Riccardo Sisto, ”dspin: A dynamic extension of spin,” in Proc. 6th SPIN Workshop, Lecture Notes in Computer Science, 1999, Vol. 1680, pp. 261–276.
[36] Radu Iosif and Riccardo Sisto, ”Using garbage collection in model checking,” in Proc. 7th SPIN Workshop, Lecture Notes in Computer Science, 2000, Vol. 1885, pp. 20–33. · Zbl 0976.68574
[37] Roby Joehanes, ”Incorporating UML State Charts into Bandera,” PhD thesis, Kansas State University, 2002, ”(Master of Science thesis).
[38] T. Lev-Ami and M. Sagiv, ”TVLA: A system for implementing static analyses,” in Proceedings of the 7th International Static Analysis Symposium (SAS’00), 2000. · Zbl 0966.68580
[39] Tim Lindholm and Frank Yellin, The Java Virtual Machine Specification, Sun Microsystems, Inc., 1997.
[40] Alberto Lluch-Lafuente, Stefan Edelkamp, and Stefan Leue, ”Partial order reduction in directed model checking,” in Proceedings of the 9th International SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, Vol. 2318, 2002. · Zbl 1077.68693
[41] L. Mounier M. Bozga, and S. Graf, ”IF2.0: A validation environment for component-based real-time systems,” in Proceedings of the Fourteenth International Conference on Computer-Aided Verification (CAV 2002) (LNCS 2404), July 2002. · Zbl 1010.68751
[42] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991. · Zbl 0753.68003
[43] S.S. Muchnick, Advanced Compiler Design and Implementation, Morgan Kaufmann Publishers, 1997.
[44] Rocco De Nicola and Frits Vaandrager, ”Three logics for branching bisimulation,” in Proceedings of 5th Annual IEEE Symposium on Logic in Computer Science, 1990, pp. 118–129. · Zbl 0886.68064
[45] S. Owre, J. M. Rushby, and N. Shankar, ”PVS: A prototype verification system,” in Proceedings of the 1th International Conference on Automated Deduction (LNCS 607), 1992.
[46] Corina S. Pasareanu, Matthew B. Dwyer, and Willem Visser, ”Finding feasible counter-examples when model checking java programs,” in Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, Lecture Notes in Computer Science, Vol. 2031, 2001. · Zbl 0978.68641
[47] Amir Pnueli, ”Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends,” Current Trends in Concurrency, Lecture Notes in Computer Science, pp. 510–584, 1986.
[48] Corina S. Păsăreanu, Matthew B. Dwyer, and Willem Visser, ”Finding feasible counter-examples when model checking abstracted Java programs,” in Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science. Springer-Verlag, April 2001. · Zbl 0978.68641
[49] S. Stoller, ”Model-checking multi-threaded distributed Java programs,” in K. Havelund, John Penix, and Willem Visser, (Eds.), Proceedings of Seventh International SPIN Workshop, volume 1885 of Lecture Notes in Computer Science, Springer-Verlag, 2000, pp. 224–244. · Zbl 0976.68556
[50] Oksana Tkachuk, Adapting Side-effects Analysis for Java Environment Generation, PhD thesis, Kansas State University, 2003, ”(Master of Science thesis).
[51] Oksana Tkachuk and Matthew B. Dwyer, ”Adapting side effects analysis for modular program model checking,” in Proceedings of the Fourth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, September 2003.
[52] Oksana Tkachuk, Matthew B. Dwyer, and Corina S. Păsăreanu, ”Automated environment generation for software model checking,” in Proceedings of the Fourth joint meeting of the European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, October 2003.
[53] Raja Valle-Rai, Laurie Hendren, Vijay Sundaresan, Patrick Lam, Etienne Gagnon, and Phong Co, ”Soot - a Java optimization framework,” in Proceedings of CASCON’99, November 1999.
[54] W. Visser, G. Brat, K. Havelund, and S. Park, ”Model checking programs,” in Proceedings of the 15th IEEE International Conference on Automated Software Engineering, September 2000.
[55] Eran Yahav, ”Verifying safety properties of concurrent Java programs using 3-valued logic,” in Proceedings of the ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, Jan 2001, pp. 27–40. · Zbl 1323.68183
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.