A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness
Model checking is an automatic technique for software verification through which all reachable states are generated from an initial state to finding errors and desirable patterns. In the model checking approach, the behavior and structure of system should be modeled. Graph transformation system is a...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Shahrood University of Technology
2020-04-01
|
| Series: | Journal of Artificial Intelligence and Data Mining |
| Subjects: | |
| Online Access: | http://jad.shahroodut.ac.ir/article_1664_8d28118e956a6dd570d11c401d1566e4.pdf |
| _version_ | 1830350513740185600 |
|---|---|
| author | N. Rezaee H. Momeni |
| author_facet | N. Rezaee H. Momeni |
| author_sort | N. Rezaee |
| collection | DOAJ |
| description | Model checking is an automatic technique for software verification through which all reachable states are generated from an initial state to finding errors and desirable patterns. In the model checking approach, the behavior and structure of system should be modeled. Graph transformation system is a graphical formal modeling language to specify and model the system. However, modeling of large systems with the graph transformation system suffers from the state space explosion problem which usually requires huge amounts of computational resources. In this paper, we propose a hybrid meta-heuristic approach to deal with this searching problem in the graph transformation system because meta-heuristic algorithms are efficient solutions to traverse the graph of large systems. Our approach, using Artificial Bee Colony and Simulated Annealing, replaces a full state space generation, only by producing part of it checking the safety, and finding errors (e.g., deadlock). The experimental results show that our proposed approach is more efficient and accurate compared to other approaches. |
| first_indexed | 2024-12-20T00:22:17Z |
| format | Article |
| id | doaj.art-78050ff36c054ec4858381d50e835a3b |
| institution | Directory Open Access Journal |
| issn | 2322-5211 2322-4444 |
| language | English |
| last_indexed | 2024-12-20T00:22:17Z |
| publishDate | 2020-04-01 |
| publisher | Shahrood University of Technology |
| record_format | Article |
| series | Journal of Artificial Intelligence and Data Mining |
| spelling | doaj.art-78050ff36c054ec4858381d50e835a3b2022-12-21T20:00:10ZengShahrood University of TechnologyJournal of Artificial Intelligence and Data Mining2322-52112322-44442020-04-018218919910.22044/jadm.2019.7564.19001664A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock FreenessN. Rezaee0H. Momeni1Department of Computer Engineering, Golestan University ,Gorgan, Iran.Department of Computer Engineering, Golestan University ,Gorgan, Iran.Model checking is an automatic technique for software verification through which all reachable states are generated from an initial state to finding errors and desirable patterns. In the model checking approach, the behavior and structure of system should be modeled. Graph transformation system is a graphical formal modeling language to specify and model the system. However, modeling of large systems with the graph transformation system suffers from the state space explosion problem which usually requires huge amounts of computational resources. In this paper, we propose a hybrid meta-heuristic approach to deal with this searching problem in the graph transformation system because meta-heuristic algorithms are efficient solutions to traverse the graph of large systems. Our approach, using Artificial Bee Colony and Simulated Annealing, replaces a full state space generation, only by producing part of it checking the safety, and finding errors (e.g., deadlock). The experimental results show that our proposed approach is more efficient and accurate compared to other approaches.http://jad.shahroodut.ac.ir/article_1664_8d28118e956a6dd570d11c401d1566e4.pdfsoftware verificationmodel checkingstate space explosionmeta-heuristic approachesgraph transformation system |
| spellingShingle | N. Rezaee H. Momeni A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness Journal of Artificial Intelligence and Data Mining software verification model checking state space explosion meta-heuristic approaches graph transformation system |
| title | A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness |
| title_full | A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness |
| title_fullStr | A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness |
| title_full_unstemmed | A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness |
| title_short | A Hybrid Meta-heuristic Approach to Cope with State Space Explosion in Model Checking Technique for Deadlock Freeness |
| title_sort | hybrid meta heuristic approach to cope with state space explosion in model checking technique for deadlock freeness |
| topic | software verification model checking state space explosion meta-heuristic approaches graph transformation system |
| url | http://jad.shahroodut.ac.ir/article_1664_8d28118e956a6dd570d11c401d1566e4.pdf |
| work_keys_str_mv | AT nrezaee ahybridmetaheuristicapproachtocopewithstatespaceexplosioninmodelcheckingtechniquefordeadlockfreeness AT hmomeni ahybridmetaheuristicapproachtocopewithstatespaceexplosioninmodelcheckingtechniquefordeadlockfreeness AT nrezaee hybridmetaheuristicapproachtocopewithstatespaceexplosioninmodelcheckingtechniquefordeadlockfreeness AT hmomeni hybridmetaheuristicapproachtocopewithstatespaceexplosioninmodelcheckingtechniquefordeadlockfreeness |