Stepwise verification of statecharts specification using state abstraction

Abstract

Model checking is an automated procedure for verifying a system. However model checking has a state explosion problem in generating a system model used in the model checking process. In this paper we develop an efficient procedure for the verification of a Statecharts specification by the model checking method. We propose a state abstraction method for obtaining an abstract Statecharts utilizing the hierarchical structure of Statecharts. Through the state abstraction method we can reduce the state space of system, thus alleviating state explosion from which the model checking suffers. Also we show that the model checking procedure with abstract Statecharts is conservative for verification of ∀CTL properties. To compensate for the conservative model checking procedure, we suggest a stepwise verification procedure. To demonstrate the applicability of our method, we verify an example system using the SMV model checker. For this purpose, we translate the Statecharts specification into an SMV program. Our experiment shows that system can be checked with a reduced state space.