Heuristic Search with Java PathFinder Using Cutoff Policy
-
- MAEOKA Jun
- Yokohama Research Laboratory, Hitachi, Ltd. The University of Electro-Communications
-
- TANABE Yoshinori
- National Institute of Informatics
-
- ISHIKAWA Fuyuki
- The University of Electro-Communications National Institute of Informatics
Bibliographic Information
- Other Title
-
- Java PathFinderにおける探索打ち切りポリシーを用いたヒューリスティック探索
Description
Software model checkers such as Java PathFinder (JPF) can discover errors in software during the test phase. However, the state space explosion is a serious problem.Various heuristic search methods, which explore the state space based on given priority function, have been proposed to solve this problem. The efficiency of a heuristic search depends on target programs. Therefore, we need various methods and heuristic functions for applying the target programs. This paper proposes a heuristic search method based on space limited search. While the existing heuristic methods control the search order with given priority values for the states, the proposed method uses search cutoff policy. It cuts off the forward search beyond the state whose probability to reach error state is evaluated low. We enhanced the JPF search engine with the proposed method to evaluate our approach. We examined our method comparing to the existing heuristic methods with test programs written in Java which are designed to evaluate model checkers. Experimental results show that the performance of our method is more than twice as much as the existing heuristic search in many cases. Therefore, the proposed method enlarges the applications of heuristic search.
Journal
-
- Computer Software
-
Computer Software 30 (3), 3_109-3_122, 2013
Japan Society for Software Science and Technology
- Tweet
Details 詳細情報について
-
- CRID
- 1390282679714791808
-
- NII Article ID
- 130004549315
-
- ISSN
- 02896540
-
- Text Lang
- ja
-
- Article Type
- journal article
-
- Data Source
-
- JaLC
- CiNii Articles
- KAKEN
-
- Abstract License Flag
- Disallowed
