| 研究課題/領域番号 |
15K00089
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
渡部 卓雄 東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | 広域自己反映計算 / アクターモデル / 動的適応 / 実行時検証 / 形式仕様記述 |
|---|
| 研究実績の概要 |
初年度は主に基盤となる個別技術についての研究にあてた．具体的には，(A)実行時検証に適した広域自己反映計算系の構成方式の実現と評価，および(B)安全性に関する性質の記述形式および検証手法の提案をそれぞれ行った．それぞれの詳細は以下の通りである．
(A) 研究代表者が前年度までに行ってきたアクターモデル上の自己反映計算モデルの研究にもとづき，プログラミング言語Erlangによる広域自己反映計算機構の実装とその評価を行った．具体的には，変化する実行環境への動的適応機構を対象に，そのオーバーヘッドを評価項目とした．本研究の特徴は，複数の計算主体（アクター等）からなる系に関する自己反映計算を扱うことにあるが，特にアクターモデルのような非同期通信にもとづく系の場合，通信の遅れを考慮する必要がある．本研究では複数個のアクターからなる系の動的適応を楽観的なアルゴリズムを用いて実装し，適応に伴う同期に必要なメッセージ数や再実行のオーバーヘッドが現実的な範囲内にあることを明らかにした．
(B) アクターモデルにもとづく並行計算系を証明支援系Coqを用いて検証するためのライブラリActarioを実装し，例題を通してその有効性を明らかにした．アクターモデルではアクターの名前（アドレス）の一意性を仮定しているが，Coqのような証明支援系による検証を行う上で，その形式化が問題となることがある．Actarioではアクターの名前の生成方式を定め，その方式で生成される名前の一意性をCoqで証明している．これにより，複雑な系を表現する場合においても名前付けが問題とならないことを示した．加えて，現実的な分散システムについての実行時検証方式の提案に向けて，必ずしも信頼できない実行系（例えば人間等）に基づくシステムを並行計算系としてモデル化し，欠陥に対する耐性解析を行う手法を提案した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
研究実績の概要で述べているように，基盤となる個別技術についての研究については順調に成果を得ている．これは当初に計画に沿ったものであるため，順調に進展していると判断した．
|
| 今後の研究の推進方策 |
平成28年度以降は，初年度の成果をもとに，いくつかの具体的な分散計算系をターゲットとして，提案手法の有効性を示す．また，初年度の(B)における検討結果をもとに(A)で実装したシステムの実行時検証方式を検討する．これにより提案している広域自己反映計算手法が適応的な分散・並行計算系に対する実行時検証の効率向上に寄与することを明らかにしていく．
具体的な対象の一つとして，初年度の発表論文において例題として扱った適応的センサネットワークを扱う．これについては，現在までに設備備品費で購入した16台のマイクロプロセッサボード上に提案システムの実装と予備的な実験を行っている．
|
| 次年度使用額が生じた理由 |
実験に用いるマイクロプロセッサーボードに用いるための周辺機器（センサーボード）について，当初予定していたものよりもやや低価格かつ高性能のものが発売されたため．
|
| 次年度使用額の使用計画 |
今後計画している計算機(TSUBAME)使用料に充て，実験規模の拡大を検討する．
|
