2017 Fiscal Year Research-status Report
| Project/Area Number |
16K00109
|
|---|
| Research Institution | Tsurumi University |
|---|
Principal Investigator |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 大学院理学研究院, 教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | モデル検査 / Java / ソフトウェア |
|---|
| Outline of Annual Research Achievements |
本研究課題は，on-the-fly ソフトウェアモデル検査 (OSMC) のアルゴリズムの開発を行うことを目的としている．まず，平成28年度に行った基本アルゴリズムの検討結果をベースに，その実装を行った．
まず，懸案であった，キャッシュ情報が得られない場合の対処として，以下の2つのオプションをそれぞれ実装し，結果を比較した．(1) 探索を再実行する (2) 1回目に復元用の情報をあらかじめ保存しておき，2回目には復元を実施する．その結果，論理式および探索空間に依存して，どちらも有利となる場合があり得ることがわかった．そこで，これらを融合させた方式として，一定の遷移回数ごとに復元ポイントを用意し，その点からは再実行を行う方式として，遷移回数の間隔はパラメタライズできるような実装を行った．これによって，実質的に両者の選択が可能となった．この選択に関しての基準を設定していくことは，今後の課題である．
もう一つの懸案であった，Java PathFinder (JPF) 実装上の最適化によって，複数回の遷移で作成される状態が異なることへの対処を行った．当初はJPFの状態作成基準に手を入れることを検討したが，実装上の困難さから，以下の方式に切り替えた．リスナーを利用することで，JPFの状態作成の判断をモニターし，1回目の記録を参照することで必要な箇所を特定し，強制的な遷移の中断を行う方法である．
アルゴリズムの形式検証については，前年度に引き続き，Coqにおける形式化を進めた．平成28年度に実施した，Petri-netにおける検証で用いた技術を状態遷移系に対して適用できるように変更を行った．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
基本アルゴリズムの実装が (最適化等でまだ改善の余地はあるものの) 一応の完成をみたため，おおむね順調であると判断する．当初計画していた強公平性条件の実装を行うことができなかったが，弱公平性部分は先行して実施しているので，平成30年度での実施は可能であると考えている．
|
| Strategy for Future Research Activity |
基本アルゴリズムを実装したものの，コードにはスタイルおよび実行速度の両面から改良すべき余地が残っているため，これを優先して作業する．現状のままでも進めることはできるが，手戻りの可能性を減らすためである．その後，弱公平性条件の実装を，強公平性条件にも対応させるように変更を行う．並行して，誤り発見に関する最適化オプションの実現に向けて検討を行う．
|
| Causes of Carryover |
研究発表および情報収集のために予定していた海外学会への参加が実現できなかったためである．今年度に実施予定としている．
|
