Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization
Model checking is a formal and automated verification technique to show that a software system behaves in accordance with the given specification. Traditional model checking uses exhaustive search techniques for finding violative behaviours of the specification. The techniques, however, often do not...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Taylor & Francis Group
2022-03-01
|
| Series: | Journal of Information and Telecommunication |
| Subjects: | |
| Online Access: | https://www.tandfonline.com/doi/10.1080/24751839.2022.2047470 |
| _version_ | 1818774736072605696 |
|---|---|
| author | Tsutomu Kumazawa Munehiro Takimoto Yasushi Kambayashi |
| author_facet | Tsutomu Kumazawa Munehiro Takimoto Yasushi Kambayashi |
| author_sort | Tsutomu Kumazawa |
| collection | DOAJ |
| description | Model checking is a formal and automated verification technique to show that a software system behaves in accordance with the given specification. Traditional model checking uses exhaustive search techniques for finding violative behaviours of the specification. The techniques, however, often do not work for huge systems because it demands a huge amount of computational resources. Search-Based Software Engineering is known to effectively solve many software engineering problems including model checking. It pursues the good balance between efficiency and qualities of solutions by using swarm intelligence and metaheuristic search methodologies. This article focuses on the state-of-the-art model checking with Ant Colony Optimization. Ant Colony Optimization is a metaheuristic, population-based and stochastic optimization algorithm. We propose two exploration strategies to further improve the balance in model checking based on Ant Colony Optimization. The proposed strategies introduce different kinds of randomized selection mechanisms to diversify solutions found by many agents. The strategies help the search algorithm extend the reachable regions effectively. Through numerical experiments, we confirmed that the proposed strategies require less computation time and memory as compared to the existing model checking with Ant Colony Optimization at the cost of finding slightly less qualified solutions. |
| first_indexed | 2024-12-18T10:45:53Z |
| format | Article |
| id | doaj.art-b2821519d0514485b8045b5623148126 |
| institution | Directory Open Access Journal |
| issn | 2475-1839 2475-1847 |
| language | English |
| last_indexed | 2024-12-18T10:45:53Z |
| publishDate | 2022-03-01 |
| publisher | Taylor & Francis Group |
| record_format | Article |
| series | Journal of Information and Telecommunication |
| spelling | doaj.art-b2821519d0514485b8045b56231481262022-12-21T21:10:33ZengTaylor & Francis GroupJournal of Information and Telecommunication2475-18392475-18472022-03-0111910.1080/24751839.2022.2047470Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimizationTsutomu Kumazawa0Munehiro Takimoto1Yasushi Kambayashi2Software Research Associates, Inc., Tokyo, JapanTokyo University of Science, Chiba, JapanNippon Institute of Technology, Saitama, JapanModel checking is a formal and automated verification technique to show that a software system behaves in accordance with the given specification. Traditional model checking uses exhaustive search techniques for finding violative behaviours of the specification. The techniques, however, often do not work for huge systems because it demands a huge amount of computational resources. Search-Based Software Engineering is known to effectively solve many software engineering problems including model checking. It pursues the good balance between efficiency and qualities of solutions by using swarm intelligence and metaheuristic search methodologies. This article focuses on the state-of-the-art model checking with Ant Colony Optimization. Ant Colony Optimization is a metaheuristic, population-based and stochastic optimization algorithm. We propose two exploration strategies to further improve the balance in model checking based on Ant Colony Optimization. The proposed strategies introduce different kinds of randomized selection mechanisms to diversify solutions found by many agents. The strategies help the search algorithm extend the reachable regions effectively. Through numerical experiments, we confirmed that the proposed strategies require less computation time and memory as compared to the existing model checking with Ant Colony Optimization at the cost of finding slightly less qualified solutions.https://www.tandfonline.com/doi/10.1080/24751839.2022.2047470Swarm intelligenceant colony optimizationmodel checkingstate explosion problemsearch-based software engineering |
| spellingShingle | Tsutomu Kumazawa Munehiro Takimoto Yasushi Kambayashi Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization Journal of Information and Telecommunication Swarm intelligence ant colony optimization model checking state explosion problem search-based software engineering |
| title | Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization |
| title_full | Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization |
| title_fullStr | Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization |
| title_full_unstemmed | Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization |
| title_short | Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization |
| title_sort | exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization |
| topic | Swarm intelligence ant colony optimization model checking state explosion problem search-based software engineering |
| url | https://www.tandfonline.com/doi/10.1080/24751839.2022.2047470 |
| work_keys_str_mv | AT tsutomukumazawa explorationstrategiesforbalancingefficiencyandcomprehensibilityinmodelcheckingwithantcolonyoptimization AT munehirotakimoto explorationstrategiesforbalancingefficiencyandcomprehensibilityinmodelcheckingwithantcolonyoptimization AT yasushikambayashi explorationstrategiesforbalancingefficiencyandcomprehensibilityinmodelcheckingwithantcolonyoptimization |