Application of automated environment generation to commercial software

Model checking can be an effective technique for detecting concurrency-related errors in software systems. However, due to scalability issues, to handle industrial-strength software, model checking needs to be combined with powerful reduction techniques. In this work, we applied modular model checking to detect errors in Interstage Business Process Management (I-BPM) software, a Java client-server application spanning more than 500,000 lines of code. To model check a separate module, one needs to represent its context of execution, i.e., its environment. Environment generation is a significant challenge, since the environment is to be general enough to uncover the module's errors, yet restrictive enough to allow tractable model checking.In this paper, we present an experimental study that demonstrates the effectiveness of environment generation as a reduction technique in general and the effectiveness of automated environment generation in particular. Since model checking of the original application was intractable, we compared performance of automatically generated environments to environments written previously by hand. Automatic environments were obtained using Bandera Environment Generator (BEG). We present results of modular verification for both manual and automatic environments. The results show that automatically generated environments produce systems with a smaller state space, yet, for faulty modules, uncover the errors and, for error-free modules, produce coverage similar to manual environments.