combining environment generation and slicing for modular software model checking
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)
environment generation slicing modular model checking