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 th...

• Type: Conference
• Year: 2006
• Where: ISSTA
• Authors: Oksana Tkachuk, Sreeranga P. Rajan
• Keywords: Environment Generation, ISSTA 2006, Model Checking, Model Checking Needs