| 研究課題/領域番号 |
26280019
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
|
|---|
| 研究分担者 |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
ARTHO Cyrille 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 主任研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学系, 特任教授 (60443199)
山形 頼之 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 主任研究員 (40415758)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア |
|---|
| 研究実績の概要 |
研究期間全体を通して、以下の3つの部品それぞれに対応するサブプロジェクトに分割して研究を進めている。(1) net-iocache: ネットワーク環境において検査対象を管理するためのJava Pathfinder(JPF)拡張。(2) net-monitor: JPF内外のネットワークプロセスからイベントを収集し、実行監視による実行時検査を行う部分。最終的にはnet-iocacheと統合される。(3) peer-monitor: 通信相手のプロセスからnet-monitorにイベントを送るツール。
(1)については、我々が先行研究課題でネットワークアプリケーションのモデル検査のために開発したnet-iocacheを、イベント取得や他コンポーネントとの連携、より柔軟なバックトラッキングに対応できるように再設計した。具体的には、アクション・スコープという概念を導入して、これを軸に既存のコードを整理・構造化・拡張した。これらの成果はnet-iocache v2として論文にまとめ、発表することを予定している。(2)については、実行監視部分とモデル検査器部分との連携の基本設計を行った。次年度にプロトタイプ実装および、単純な例を用いた評価を予定している。また、実行監視に用いることが期待されるログ収集ツール、特にfluentdに関する調査を行った。(3)については実行監視のための論理/形式体系として、CSPを拡張した言語の検査器のプロトタイプをScala上に実装した。
平成26年度は初年度のため、基本設計に関する調査・検討が主な内容となった。そのこともあり、今年度発表した論文は最終的な完成物に直結するものというよりは、むしろ先行研究課題からの継続も含め、上記研究の過程で得られた副次的な成果という側面が強い。
研究協力者 馬雷 (千葉大学) ヴァイテル・フランツ (千葉大学) セビ・ナジム (東京大学)
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で述べた3項目(1)(2)(3)ともに、年度当初に予定していた計画をほぼ順調に達成している。特に(1)については、先行研究課題からの継続という側面が強いこともあり、実装面も含めてとりわけ順調に進んでいる。
|
| 今後の研究の推進方策 |
平成27年度から研究分担者のうち1名が関東地域から関西地域へと異動になったことで、前年度と同様に全員が出席する形でのミーティングを同回数開催することは、予算的に難しくなると考えられる。一部のミーティングについてはビデオ会議システム等を利用して行うことを考えている。
|
| 次年度使用額が生じた理由 |
当初計画では平成26年度後半からと考えていたポスドク研究者の雇用が、実際には11月中旬からとなったため。
また、平成26年度に採択された論文の国際会議が国内で開催されたものであったため。
|
| 次年度使用額の使用計画 |
平成27年度分として請求した助成金と併せ、主に平成27年度のポスドク研究者雇用費として、また国際会議に投稿を準備している論文の発表のための旅費として使用する。論文の採択状況によっては、平成28年度分の前倒し使用も視野に入れている。
|
