2013 Fiscal Year Annual Research Report
クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法
| Project/Area Number |
23240003
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
横山 重俊 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (10600968)
ARTHO Cyrille 独立行政法人産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| Project Period (FY) |
2011-04-01 – 2016-03-31
|
| Keywords | 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング |
|---|
| Research Abstract |
研究実施計画に記載の項目に従って進捗を述べる．
(1) ノンブロッキングIO については，実アプリケーションへの適用を行い，OSSのウェブサーバの不具合を検出して，有用性を示した．また，UDPプロトコルサポートを実現した．さらに，当初計画にない以下の2点を追加実施した．一つはnet-iocacheの設計見直しで，SUTとピアが整合していることに関する制約を緩和することを目指している．もう一つは，中心化方式からの技術の取り込みであり，具体的にはnative codeの自動処理を可能にする拡張を開始し，設計までを行った．
(2) モデルベーステストツールModbatは，前年度のプロトタイプを発展させ，Scala上に実現したDSLを持つテストツールとして公開した．JPF用のjava.nioライブラリの他，SAT solverへの適用でも実際に不具合を検出し，有効性を示した．
(3) マスター・スレーブモデル検査では，検証モデルを同期通信から非同期通信に変更した．アルゴリズムの再定義を完了し，その正当性も示した．プロトタイプ実装を行い評価した結果，性能を得るために設計変更が必要であることが判明したため，具体案の検討を行った．
(4) ディプロイメントについては，引き続き運用時の環境構築に力点をおいている．この見地から，新しい仮想マシン間通信方法の考案，および，運用時の通信を監視するアーキテクチャの考案を行った．また，事例研究として，OpenFlow方式のSDNネットワークモデルを本課題のライブラリを用いて検証し，プロトコルサポート等に関するフィードバックを得た．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度の研究遂行に伴い，中期的に重点項目と考えている多様なプロトコルへの対応の検討を行った結果，net-iocacheの再構築が重要であるとの認識で研究グループ内が一致し，当初の予定にない研究項目として取組を行った．また，中心化方式の一部取り込みも，予定外の項目であり，検証者に要求する工数を大きく下げるために有用である．それだけではなく，本年度より開始したNASAの研究者との協力の枠組みによるものでもあり，協力関係の発展という見地からも重要視する価値があると判断している．これらの2件を追加した結果，個々の研究項目の状況も勘案しつつ，本年度における優先度を再検討した．この結果，当初予定していた本年度の実施項目からJPF7, ModbatのZookeeper APIへの適用等の数項目が落とされることになったが，全体的には，当初予定した項目を質的に上回る内容の実現および新しい取組の開始ができたと考えている．
|
| Strategy for Future Research Activity |
研究内容としては，基本的に従来の項目を引き継いでいくが，特にnet-iocacheの再設計を重視していく．これは単にソフトウェアの設計のやり直しではなく，(中心化方式に対して) 本方式が必然的に持っている整合性確保のとらえ方の問題である．この意味で，実装だけでなく，理論面の整備もあわせて進める．
研究体制については，NASAをはじめとした海外でJPFを用いて研究しているグループとの連携をより一層強化していく．JPF workshop への継続的な参加の他，昨年日本で実施されたJPFセミナーのような企画を，本課題の枠組みの中で実施していくことも視野に検討する．また，実装技術に関しては，本課題に近い興味を持っている大学院生等の研究協力者の方向と合致する部分を見極めて，双方の研究において役立つような効果が得られるようにする．さらに，特にモデルベーステストに関しては，本課題の研究項目の中でも，実際の開発現場におけるニーズに近いものがある．現場の技術者の経験をフィードバックさせられるような仕組みを模索する．
|
