Gustavo Quiros

 

Static Byte-Code Analysis for State Space Reduction

 

Abstract:

 

NIPS is a virtual machine for the generation of
state-transition systems of concurrent models, and is designed to serve
as a foundation for the development of model checking applications. Like
any explicit-state representation, the transition systems produced by
NIPS suffer from the state-explosion problem, by which models have
exponentially large state spaces. This work is dedicated to the
reduction of the effect of the state-explosion problem in NIPS.

State space reduction may be applied to the full state-transition
system, producing the reduced system from it. However, this approach is
not practical because the peak memory requirements are not improved, and
they are precisely the most important limitation of model checking
applications. In order to present a practical and useful solution, the
reduction must be done on-the-fly, producing the reduced system directly
from the model without the need to construct the full state-transition
system. For this, static analysis of the code is usually employed in
order to gather information which will be used when computing the
reduced system.

NIPS features a byte-code language for encoding concurrent models.
High-level modeling languages may be compiled to this byte-code, and the
interpretation of the bytecode by the machine results in the
construction of the model's state space representation. This
architecture allows us to implement on-the-fly reductions merely by
transforming the byte-code to another whose state-transition system is a
reduced version of the original, and employing information gathered from
static analysis of the byte-code in the process. The main goal of this
work is to implement state space reductions for NIPS in this way.