2016 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 | モデル検査 / ソフトウェア検証 / アルゴリズム |
|---|
| Outline of Annual Research Achievements |
本研究課題は，on-the-fly ソフトウェアモデル検査 (OSMC) のアルゴリズムの開発を行うことを目的としている．OSMCにおいて，対象状態遷移系での遷移を実行コストと，仕様記述論理式から生成されるオートマトンの実行コストの差に着目しているため，まず，実装対象モデル検査器である Java PathFinder 上でのこの差の実測をおこなった．この計測結果に基づき，小さなプログラムを利用して，想定するアルゴリズムによって生成されるはずの遷移系で動作させるシミュレーションを実施した．実際に性能改善に結びつくことを確認したが，検証対象論理式による差が，当初予想以上に大きかったため，実際によく用いられる論理式に特化したアルゴリズムの最適化の優先度を上げることとした．
次に予定していたアルゴリズムの実装には，延期することとした．理由は，Java PathFinderの実装との齟齬が発見されたため，修正が必要となることがわかったためと，最終的に必要となる弱公平性の下での検証アルゴリズムの効率的な実装を優先するためであり，後者については実装を完成させた．延期したアルゴリズムの実装は，平成29年度に実施する予定である． 本研究のもうひとつの柱であるアルゴリズムの形式検証については，そのプラットフォームであるCoqにおける形式化に取り組んだ．対象とするデータ構造は状態遷移系であるが，担当する研究分担者が並行して取り組んでいる，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
基本アルゴリズムの実装を延期した点が当初予定よりは遅れているが，その代わりに，シミュレーションを用いた効果の測定と，弱公平性アルゴリズムの実装を先行して行ったので，総合的に見れば，ほぼ予定していた進捗を達成していると考える．
|
| Strategy for Future Research Activity |
延期した基本アルゴリズムの実装を，第一優先として，作業を進める．28年度のシミュレーションから，論理式のパターンに応じた最適化の重要性も認識されたが，まずは基本アルゴリズムに集中し，その後に検討を行うこととする予定である．
|
| Causes of Carryover |
開発順の見直しに伴い，当初予定していた国際学会への参加を見送ったため，次年度使用額が生じた．
|
| Expenditure Plan for Carryover Budget |
当該開発順の見直しは，開発項目の延期であるため，今年度に開発を行い，その結果に基づいて適切な国際学会に参加することで使用する計画である．
|
Research Products
(5 results)
