Fine-Grained Model Slicing for Faster Verification

Abstract

In this age of automatization and digitization a majority of organizations relies on large, complex software systems. For many of these organizations, it is critical that their systems behave as expected, as unexpected behavior may result in financial loss, lawsuits, or even human casualties. With software becoming ubiquitous, software validation is growing increasingly important. But software verification is costly, and the resources required to thoroughly check systems are not always available.

We propose model slicing as a technique for increasing the efficiency of bounded model checking, a common method for software verification. Model slicing has been successfully applied to speeding up explicit and symbolic model checking, but the question of whether it will benefit bounded model checking, commonly implemented with highly optimized, state-of-the-art SMT-solvers, is currently unanswered. We provide a model slicing algorithm more fine-grained than the ones found in today's literature, and implement it into a mode slicing tool for Rebel, a modeling language with built-in validation engine based on bounded model checking.

To test our hypothesis we have benchmarked our tool against unsliced models. These benchmarks show that model slicing has the potential to let us check larger problem instances and use higher path bounds. For small and shallow problem instances, however, unsliced bounded model checking outperforms our tool on account of the overhead of slicing. We conclude that bounded model checking can gain a lot from model slicing, depending on model properties such as size, modularity and expected bug depth.