Handling state space explosion in verification of component-based systems: A review

TL;DR

This paper reviews various methods for mitigating state-space explosion in model-checking of component-based systems, highlighting their principles, similarities, limitations, and future research challenges.

Contribution

It provides a comprehensive classification and analysis of SSE reduction techniques specifically in the context of component-based software verification.

Findings

Classifies SSE handling methods based on their principles and characteristics

Identifies limitations and challenges of current SSE reduction techniques

Highlights future research directions in SSE management for CBSD

Abstract

Component-based software development (CBSD) is an alternative approach to constructing software systems that offers numerous benefits, particularly in 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 to systematically analyze the correctness of a system. It is a bruce-force checking of the system's state space that assists to significantly expand the level of confidence in the system. Nevertheless, model-checking is limited by a critical problem called state-space explosion (SSE). To benefit from model-checking, an appropriate method is required to reduce SSE. In the past two decades, a great number of SSE reduction methods have been proposed containing many similarities, dissimilarities, and unclear concepts in some cases. This research, firstly, plans to present a review of SSE handling methods and classify them based on their similarities, principle, and characteristics. Second, it investigates the methods for handling the SSE problem in the verification process of CBSD and provides insight into the potential limitations, underlining the key challenges for future research efforts.