Handling state space explosion in component-based software verification: a review
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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Published: |
Institute of Electrical and Electronics Engineers
2021
|
| Online Access: | http://psasir.upm.edu.my/id/eprint/97497/ |
| _version_ | 1848862615256694784 |
|---|---|
| author | Nejati, Faranak Abd Ghani, Abdul Azim Ng, Keng Yap Jafaar, Azmi |
| author_facet | Nejati, Faranak Abd Ghani, Abdul Azim Ng, Keng Yap Jafaar, Azmi |
| author_sort | Nejati, Faranak |
| building | UPM Institutional Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-15T13:19:50Z |
| format | Article |
| id | upm-97497 |
| institution | Universiti Putra Malaysia |
| institution_category | Local University |
| last_indexed | 2025-11-15T13:19:50Z |
| publishDate | 2021 |
| publisher | Institute of Electrical and Electronics Engineers |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | upm-974972023-04-19T04:03:18Z http://psasir.upm.edu.my/id/eprint/97497/ Handling state space explosion in component-based software verification: a review Nejati, Faranak Abd Ghani, Abdul Azim Ng, Keng Yap Jafaar, Azmi 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. Institute of Electrical and Electronics Engineers 2021 Article PeerReviewed Nejati, Faranak and Abd Ghani, Abdul Azim and Ng, Keng Yap and Jafaar, Azmi (2021) Handling state space explosion in component-based software verification: a review. IEEE Access, 9. 77526 - 77544. ISSN 2169-3536 https://ieeexplore.ieee.org/abstract/document/9435368 10.1109/ACCESS.2021.3081742 |
| spellingShingle | Nejati, Faranak Abd Ghani, Abdul Azim Ng, Keng Yap Jafaar, Azmi Handling state space explosion in component-based software verification: a review |
| title | Handling state space explosion in component-based software verification: a review |
| title_full | Handling state space explosion in component-based software verification: a review |
| title_fullStr | Handling state space explosion in component-based software verification: a review |
| title_full_unstemmed | Handling state space explosion in component-based software verification: a review |
| title_short | Handling state space explosion in component-based software verification: a review |
| title_sort | handling state space explosion in component-based software verification: a review |
| url | http://psasir.upm.edu.my/id/eprint/97497/ http://psasir.upm.edu.my/id/eprint/97497/ http://psasir.upm.edu.my/id/eprint/97497/ |