Java PathFinderにおける探索打ち切りポリシーを用いたヒューリスティック探索
スポンサーリンク
概要
- 論文の詳細を見る
Java PathFinder (JPF)に代表されるソフトウェアモデル検査技術は，テスト工程における不具合検出に有効であるが，状態爆発への対応が課題となる．この課題を解決する手法として優先度に基づくヒューリスティック探索手法が提案されている．プログラムによって適する探索手法や優先度の付け方が異なるため，有効なヒューリスティック探索手法が多数存在することがのぞましい．本論文では，「範囲限定探索」に基づくヒューリスティック探索手法を提案する．従来手法は，ヒューリスティック関数によって各状態から不具合に早く到達できるかを見積もり，これに基づいて探索順序を決定する．これに対して提案手法では，「探索打ち切りポリシー関数」によって各状態から不具合に早く到達できるかを判断し，見込みが低い場合にはその状態からの探索を打ち切る．提案手法の有効性を検証するためにJPFに実装し，検証ツール評価用に作成されたテストプログラムを用いて既存手法との比較実験を行った．Javaによるテストプログラムを用いた実験の結果，提案手法が状態数比で2倍以上優位となるケースを確認し，ヒューリスティック探索の適用の幅が広がることを示した．
- 日本ソフトウェア科学会の論文
日本ソフトウェア科学会 | 論文
- LCDと透明弾性体の光弾性を用いたユーザインタフェース (特集 インタラクティブシステムとソフトウェア)
- Bluetoothによる位置検出
- COINSにおけるSIMD並列化(最新コンパイラ技術とCOINSによる実践)
- データ型を考慮した軽量なXML文書処理系の自動生成(ソフトウェア開発を支援する基盤技術)
- 計算と論理のための自然枠組NF/CAL(システム検証の科学技術)