Handling State Space Explosion in Component-Based Software Verification: A Review

Autor: Faranak Nejati, Abdul Azim Abd Ghani, Ng Keng Yap, Azmi Bin Jafaar
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Zdroj: IEEE Access, Vol 9, Pp 77526-77544 (2021)
Druh dokumentu: article
ISSN: 2169-3536
DOI: 10.1109/ACCESS.2021.3081742
Popis: 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. Its brute-force checking of the system’s state space 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 SSE problem in the verification process of CBSD and provides insight into the potential limitations, underlining the key challenges for future research efforts.
Databáze: Directory of Open Access Journals