Combining environment generation and slicing for modular software model checking

ABSTRACT

To be effective, software model checking needs powerful reduction techniques. In this paper, we present an experimental study that demonstrates effectiveness of environment generation combined with slicing as a model generation and reduction technique. Automatic environments were obtained using the Bandera Environment Generator (BEG) and slicing was performed using the Indus Java slicer. The results show that environment generation implemented in BEG is an aggressive reduction technique. However, it may miss behaviors in the environment and consequently in the module under analysis, making it unsafe. As such, this technique can be effective for detection of errors but not sufficient to prove their absence.Slicing, while a safe technique, may be too approximate and not scalable. Also, slicing implemented in Indus requires a closed system and cannot be safely applied to a module without its environment. In this paper, we show how environment generation and slicing can be combined to detect errors and prove their absence. We applied the combined approach to verify parts of Fujitsu's enterprise software called Interstage Business Process Management (I-BPM)

REFERENCES

• 1: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 2: G. Brat, K. Havelund, S. Park, and W. Visser. Java PathFinder - a second generation of a Java model-checker. In Proceedings of the Workshop on Advances in Verification July 2000.
• 3: John Hatcliff , Matthew B. Dwyer , Hongjun Zheng, Slicing Software for Model Construction, Higher-Order and Symbolic Computation, v.13 n.4, p.315-353, Dec. 1, 2000 [doi>10.1023/A:1026599015809]
• 4: V. Ranganath. Indus Website. http://indus.projects.cis.ksu.edu
• 5: Scott D. Stoller, Model-Checking Multi-threaded Distributed Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.224-244, August 30-September 01, 2000
• 6: O. Tkachuk. Bandera Environment Generator Website. http://beg.projects.cis.ksu.edu
• 7: Oksana Tkachuk , Sreeranga P. Rajan, Application of automated environment generation to commercial software, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146262]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

General Terms:
Verification

Keywords:
environment generation, modular model checking, slicing