| 研究課題/領域番号 |
23240003
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
ARTHO Cyrille 独立行政法人産業技術総合研究所, 情報セキュリティセンター, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| キーワード | 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング |
|---|
| 研究実績の概要 |
研究実施計画の項目に従って進捗を述べる．
(1) net-iocache v2．TCP通信に関しては，クライアント側の基本的な機能を完成させた．チャネル間依存関係に関しては，すべてのチャネルに依存関係があり得るとの仮定を置き，キャッシュは線形のものに限定し，プリフェッチも使用しないという前提で，本機能の設計，実装を行った．この範囲で正しく機能することが確認できている．
(2) モデルベーステストツールModbat．入力されたモデルからより多くのテストパスを効率的に生成するための改良を検討し，設計・実装を行った．特に，従来の同期式コールバックに加えて，非同期式コールバックを追加したことで，適用可能なアプリケーションを増すことに成功した．
(3) UDP検証．パケットの消失，重複，順序変更の3つの事象が非決定的に発生するプロトコルを解析するとの立場で研究を進めている．条件が無いと対象の遷移系の大きさが無限になってしまうので，遅延パケットの数と重複を発生させるパターンを限定 (パラメタで与える) して，遷移系を有限としたモデルを扱うこととした．この前提の下で，状態数に関する理論的な解析を行い，各パラメタが遷移系の大きさに与える影響を明らかにした．さらに，net-iocache v2 の上にUDP解析モジュールを実装し，主要なAPIに対応した．この実装を用いて，UDPによる通信を行うアプリケーションが持つ不具合を発見できることを実証した．
(4) JPF探索アルゴリズム (マスター・スレーブモデル検査)．JPFのメイン探索エンジン変更の準備として，LTLモデル検査アルゴリズムのうちのNDFSの実装と，DFSベースのヒューリスティック探索機能の実装を行った．
(5) jpf-nas, nhandler連携．基本的な検討を行ったが，いずれについてもただちに実装可能な連携は難しいとの結論となった．しかし，検討の過程で明らかになった事項のいくつかは項目(1)の設計に反映させることができた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
2014年度は，項目(1)(3)に関して大きな進捗があった．項目(1)のチャネル相互の依存関係の考慮について，前年度までは単なる構想でしかなかった．いくつかの制限を置いた上とはいえ，実際に依存関係のあるチャネルを持つアプリケーションを対象とした実装ができたことで，完成に向けての具体的な計画を立てることが可能となった．項目(3)については，理論および実装の両面で，ほぼ最終的な形となったと言える．残りの(2),(4)についても，最終年度での完成が見通せる段階に達していると評価している．
項目(5)に関しては実績があまり無かったが，もともと試行するという位置づけの計画であり，連携相手のソフトウェアの完成度の問題もあったため，やむを得なかったと考える．一方で，この項目の検討を通して項目(1)の設計上の問題点が明らかになり，これを修正することができたので，検討自体は意義があったと評価できる．
|
| 今後の研究の推進方策 |
研究項目に関しては，昨年度の検討の結果棚上げとなった項目(5)を除いて，従来の項目を引き継いでいく．最終年度となるので，各項目に関して理論・実装の両面で現在得られている結果を参照しつつ検討の方向性を整理し，年度末に向けて各項目毎に成果をまとめることができるように研究を進めていく．
研究成果の広報，普及については，当研究課題の直接のターゲットが Java PathFinder をフレームワークとした検証ツールであることを踏まえ，開発・利用者コミュニティが研究成果を容易に利用できるようにするという観点から，ドキュメントの整備やスクリプトなどの利用ツールの整備を，優先度を上げて行っていく．
|
