Title: Handling state space explosion in verification of component-based systems: A review,
Abstract: Component-based design is a different way of constructing systems which
offers numerous benefits, in particular, decreasing the complexity of system
design. However, deploying components into a system is a challenging and
error-prone task. Model checking is one of the reliable methods that
automatically and systematically analyse the correctness of a given system. Its
brute-force check of the state space significantly expands the level of
confidence in the system. Nevertheless, model checking is limited by a critical
problem so-called State Space Explosion (SSE). To benefit from model checking,
appropriate methods to reduce SSE, is required. In two last decades, a great
number of methods to mitigate the state space explosion have been proposed
which have many similarities, dissimilarities, and unclear concepts in some
cases. This research, firstly, aims at present a review and brief discussion of
the methods of handling SSE problem and classify them based on their
similarities, principle and characteristics. Second, it investigates the
methods for handling SSE problem in verifying Component-based system (CBS) and
provides insight into CBS verification limitations that have not been addressed
yet. The analysis in this research has revealed the patterns, specific
features, and gaps in the state-of-the-art methods. In addition, we identified
and discussed suitable methods to soften SSE problem in CBS and underlined the
key challenges for future research efforts.