• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2015 Fiscal Year Research-status Report

広域自己反映計算にもとづく適応的並列計算系の実行時検証とそのための仕様記述方式

Research Project

Project/Area Number 15K00089
Research InstitutionTokyo Institute of Technology

Principal Investigator

渡部 卓雄  東京工業大学, 情報理工学(系)研究科, 准教授 (20222408)

Project Period (FY) 2015-04-01 – 2018-03-31
Keywords広域自己反映計算 / アクターモデル / 動的適応 / 実行時検証 / 形式仕様記述
Outline of Annual Research Achievements

初年度は主に基盤となる個別技術についての研究にあてた.具体的には,(A)実行時検証に適した広域自己反映計算系の構成方式の実現と評価,および(B)安全性に関する性質の記述形式および検証手法の提案をそれぞれ行った.それぞれの詳細は以下の通りである.
(A) 研究代表者が前年度までに行ってきたアクターモデル上の自己反映計算モデルの研究にもとづき,プログラミング言語Erlangによる広域自己反映計算機構の実装とその評価を行った.具体的には,変化する実行環境への動的適応機構を対象に,そのオーバーヘッドを評価項目とした.本研究の特徴は,複数の計算主体(アクター等)からなる系に関する自己反映計算を扱うことにあるが,特にアクターモデルのような非同期通信にもとづく系の場合,通信の遅れを考慮する必要がある.本研究では複数個のアクターからなる系の動的適応を楽観的なアルゴリズムを用いて実装し,適応に伴う同期に必要なメッセージ数や再実行のオーバーヘッドが現実的な範囲内にあることを明らかにした.
(B) アクターモデルにもとづく並行計算系を証明支援系Coqを用いて検証するためのライブラリActarioを実装し,例題を通してその有効性を明らかにした.アクターモデルではアクターの名前(アドレス)の一意性を仮定しているが,Coqのような証明支援系による検証を行う上で,その形式化が問題となることがある.Actarioではアクターの名前の生成方式を定め,その方式で生成される名前の一意性をCoqで証明している.これにより,複雑な系を表現する場合においても名前付けが問題とならないことを示した.加えて,現実的な分散システムについての実行時検証方式の提案に向けて,必ずしも信頼できない実行系(例えば人間等)に基づくシステムを並行計算系としてモデル化し,欠陥に対する耐性解析を行う手法を提案した.

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

研究実績の概要で述べているように,基盤となる個別技術についての研究については順調に成果を得ている.これは当初に計画に沿ったものであるため,順調に進展していると判断した.

Strategy for Future Research Activity

平成28年度以降は,初年度の成果をもとに,いくつかの具体的な分散計算系をターゲットとして,提案手法の有効性を示す.また,初年度の(B)における検討結果をもとに(A)で実装したシステムの実行時検証方式を検討する.これにより提案している広域自己反映計算手法が適応的な分散・並行計算系に対する実行時検証の効率向上に寄与することを明らかにしていく.
具体的な対象の一つとして,初年度の発表論文において例題として扱った適応的センサネットワークを扱う.これについては,現在までに設備備品費で購入した16台のマイクロプロセッサボード上に提案システムの実装と予備的な実験を行っている.

Causes of Carryover

実験に用いるマイクロプロセッサーボードに用いるための周辺機器(センサーボード)について,当初予定していたものよりもやや低価格かつ高性能のものが発売されたため.

Expenditure Plan for Carryover Budget

今後計画している計算機(TSUBAME)使用料に充て,実験規模の拡大を検討する.

  • Research Products

    (9 results)

All 2016 2015 Other

All Journal Article (2 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 2 results,  Open Access: 1 results,  Acknowledgement Compliant: 1 results) Presentation (5 results) (of which Int'l Joint Research: 3 results) Remarks (2 results)

  • [Journal Article] アクターモデルに基づく並行文脈指向プログラミング機構の実装と評価2016

    • Author(s)
      竹野創平, 渡部卓雄
    • Journal Title

      コンピュータソフトウェア

      Volume: 33 Pages: 167-180

    • DOI

      10.11309/jssst.33.1_167

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] A Model-Checking Based Approach to Robustness Analysis of Procedures under Human-Made Faults2015

    • Author(s)
      Naoyuki Nagatou and Takuo Watanabe
    • Journal Title

      International Journal of Industrial Engineering: Theory, Applications and Practice

      Volume: 22 Pages: 494-508

    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Emfrp: A Functional Reactive Programming Language for Small-Scale Embedded Systems2016

    • Author(s)
      Kensuke Sawada and Takuo Watanabe
    • Organizer
      Modularity 2016, Constrained and Reactive Objects Workshop (CROW 2016)[査読有]
    • Place of Presentation
      Univ. of Malaga, Malaga, Spain
    • Year and Date
      2016-03-15 – 2016-03-15
    • Int'l Joint Research
  • [Presentation] 時相論理式の反証を用いた制御器のチューニング2016

    • Author(s)
      峰尾太陽, 石井大輔, 渡部卓雄
    • Organizer
      電子情報通信学会 システム数理と応用研究会
    • Place of Presentation
      海峡メッセ下関, 山口県下関市
    • Year and Date
      2016-03-03 – 2016-03-04
  • [Presentation] A Reflective Implementation of an Actor-based Concurrent Context-Oriented System2015

    • Author(s)
      Sohei Takeno and Takuo Watanabe
    • Organizer
      14th Workshop on Adaptive and Reflective Middleware (ARM 2015)[査読有]
    • Place of Presentation
      Vancouver Marriott Hotel, Vancouver, BC, Canada
    • Year and Date
      2015-12-08 – 2015-12-08
    • Int'l Joint Research
  • [Presentation] Actario: A Framework for Reasoning About Actor Systems2015

    • Author(s)
      Shohei Yasutake and Takuo Watanabe
    • Organizer
      5th International Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE!@SPLASH 2015) [査読有]
    • Place of Presentation
      Sheraton Station Square Hotel, Pittsburgh, PA, US
    • Year and Date
      2015-10-26 – 2015-10-26
    • Int'l Joint Research
  • [Presentation] 小規模組み込みシステムにおけるFRPの応用に向けて2015

    • Author(s)
      澤田賢祐, 鈴木康平, 渡部卓雄
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会(SIGSS)
    • Place of Presentation
      熊本大学黒髪キャンパス, 熊本県熊本市
    • Year and Date
      2015-05-11 – 2015-05-12
  • [Remarks] Actario

    • URL

      https://github.com/amutake/actario

  • [Remarks] Emfrp

    • URL

      https://github.com/sawaken/emfrp

URL: 

Published: 2017-01-06  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi