Higher-Order and Symbolic Computation, 13(4)315-353
Slicing Software for Model ConstructionJohn Hatcliff, Computing and Information Sciences Department, Kansas State University, 234 Nichols Hall, Manhattan KS, 66506, USA
Matthew B. Dwyer, Computing and Information Sciences Department, Kansas State University, 234 Nichols Hall, Manhattan KS, 66506, USA
Hongjun Zheng, Computing and Information Sciences Department, Kansas State University, 234 Nichols Hall, Manhattan KS, 66506, USA
|
Abstract: Applying finite-state verification techniques (e.g.,
model checking) to software requires that program source code be
translated to a finite-state transition system that safely models
program behavior. Automatically checking such a transition system for
a correctness property is typically very costly, thus it is necessary
to reduce the size of the transition system as much as possible. In
fact, it is often the case that much of a program's source code is
irrelevant for verifying a given correctness property. In this paper, we apply program slicing techniques to remove automatically such irrelevant code and thus reduce the size of the corresponding transition system models. We give a simple extension of the classical slicing definition, and prove its safety with respect to model checking of linear temporal logic (LTL) formulae. We discuss how this slicing strategy fits into a general methodology for deriving effective software models using abstraction-based program specialization. Keywords: software verification, model-checking, state-space reduction, linear temporal logic, program slicing, program dependence graph |
This article can be downloaded [here].