| 研究課題/領域番号 |
16K00109
|
|---|
| 研究機関 | 鶴見大学 |
|---|
研究代表者 |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 大学院理学研究科, 准教授 (00291295)
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| キーワード | モデル検査 / ソフトウェア検証 / アルゴリズム |
|---|
| 研究実績の概要 |
本研究課題は，on-the-fly ソフトウェアモデル検査 (OSMC) のアルゴリズムの開発を行うことを目的としている．OSMCにおいて，対象状態遷移系での遷移を実行コストと，仕様記述論理式から生成されるオートマトンの実行コストの差に着目しているため，まず，実装対象モデル検査器である Java PathFinder 上でのこの差の実測をおこなった．この計測結果に基づき，小さなプログラムを利用して，想定するアルゴリズムによって生成されるはずの遷移系で動作させるシミュレーションを実施した．実際に性能改善に結びつくことを確認したが，検証対象論理式による差が，当初予想以上に大きかったため，実際によく用いられる論理式に特化したアルゴリズムの最適化の優先度を上げることとした．
次に予定していたアルゴリズムの実装には，延期することとした．理由は，Java PathFinderの実装との齟齬が発見されたため，修正が必要となることがわかったためと，最終的に必要となる弱公平性の下での検証アルゴリズムの効率的な実装を優先するためであり，後者については実装を完成させた．延期したアルゴリズムの実装は，平成29年度に実施する予定である． 本研究のもうひとつの柱であるアルゴリズムの形式検証については，そのプラットフォームであるCoqにおける形式化に取り組んだ．対象とするデータ構造は状態遷移系であるが，担当する研究分担者が並行して取り組んでいる，Petri-net における検証に用いられた関数群を，状態遷移系にも適用できるようにするために，ライブラリとして整備する作業を進めた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
基本アルゴリズムの実装を延期した点が当初予定よりは遅れているが，その代わりに，シミュレーションを用いた効果の測定と，弱公平性アルゴリズムの実装を先行して行ったので，総合的に見れば，ほぼ予定していた進捗を達成していると考える．
|
| 今後の研究の推進方策 |
延期した基本アルゴリズムの実装を，第一優先として，作業を進める．28年度のシミュレーションから，論理式のパターンに応じた最適化の重要性も認識されたが，まずは基本アルゴリズムに集中し，その後に検討を行うこととする予定である．
|
| 次年度使用額が生じた理由 |
開発順の見直しに伴い，当初予定していた国際学会への参加を見送ったため，次年度使用額が生じた．
|
| 次年度使用額の使用計画 |
当該開発順の見直しは，開発項目の延期であるため，今年度に開発を行い，その結果に基づいて適切な国際学会に参加することで使用する計画である．
|
