Timed CSPを用いた実時間並列システム検証プログラムの開発

• 研究課題/領域番号: 25330087
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: ソフトウェア
• 研究機関: 首都大学東京
• 研究代表者: 福永 力 首都大学東京, 理工学研究科, 教授 (00189961)
• 研究期間 (年度): 2013-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2015年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円); 2014年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円); 2013年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
• キーワード: 並列処理 / 形式手法 / CSP理論 / 失敗・発散検査 / 並列システム記述理論 / 形式理論 / timed-CSP / FDR（失敗-発散-詳細化解析） / FDR（失敗-発散-詳細化）解析 / 国際情報交換（英国、シンガポール） / 国際情報交換（英国、米国）

研究成果の概要

本研究は並列計算処理プログラムの安定動作のための設計技法（形式言語）に関するものである．複数のユニットが並列に動作すると予測できない不具合により並列計算が立ち往生してしまう．それを避けるべく並列処理部分のシーケンスをユニットごとに設計図としてまとめておき、複数のユニットが並列動作した時の全体の並列動作の流れのみを形式的に確認する方法が研究されている．本研究はシーケンスをただイベントとして記述するばかりでなく時間の概念も導入して並列処理が安定に動作するか検証しようというものである．並列処理で生じると予測されるいくつかの不具合は設計段階で予知できる技法の開発を進めることができた．

研究成果

• [学会発表] Native Pythonの並列処理 (2015)
  • 著者名/発表者名: 福永 力
  • 学会等名: 第16回CSP研究会
  • 発表場所: 東洋大学（東京都・文京区）
  • 年月日: 2015-11-21
• [学会発表] ST20プロセッサ -Real Time CSP実現に向けた取り組み (2015)
  • 著者名/発表者名: 福永 力
  • 学会等名: 第15回CSP研究会
  • 発表場所: 東洋大学（東京都・文京区）
  • 年月日: 2015-06-06
• [学会発表] CSPベースの並列処理言語の動向 (2014)
  • 著者名/発表者名: 福永 力
  • 学会等名: 第14回CSP研究会
  • 発表場所: 東洋大学・白山キャンパス
  • 年月日: 2014-11-29
• [学会発表] XMOSのコンテキストスイッチング (2014)
  • 著者名/発表者名: 福永 力
  • 学会等名: 第13回CSP研究会
  • 発表場所: 東洋大学・白山キャンパス
  • 年月日: 2014-05-24
• [学会発表] π-calculusとOccam-π (2013)
  • 著者名/発表者名: 福永 力
  • 学会等名: 第11回CSP研究会
  • 発表場所: 東洋大学・白山キャンパス
  • 招待講演