Sciweavers

Share
KBSE
2003
IEEE

Automated Environment Generation for Software Model Checking

9 years 9 months ago
Automated Environment Generation for Software Model Checking
A key problem in model checking open systems is environment modeling (i.e., representing the behavior of the execution context of the system under analysis). Software systems are fundamentally open since their behavior is dependent on patterns of invocation of system components and values defined outside the system but referenced within the system. Whether reasoning about the behavior of whole or about program components, an abstract model of the environment can be essential in enabling sufficiently precise yet tractable verification. In this paper, we describe an approach to generating environments of Java program fragments. This approach integrates formally specified assumptions about environment behavior with sound abstractions of environment implementations to form a model of the environment. The approach is implemented in the Bandera Environment Generator (BEG) which we describe along with our experience using BEG to reason about properties of several non-trivial concurrent J...
Oksana Tkachuk, Matthew B. Dwyer, Corina S. Pasare
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where KBSE
Authors Oksana Tkachuk, Matthew B. Dwyer, Corina S. Pasareanu
Comments (0)
books