Development of a validity check program for real time parallel systems using timed CSP

• Project/Area Number: 25330087
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: Tokyo Metropolitan University
• Principal Investigator: Fukunaga Chikara 首都大学東京, 理工学研究科, 教授 (00189961)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000); Fiscal Year 2014: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000); Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 並列処理 / 形式手法 / CSP理論 / 失敗・発散検査 / 並列システム記述理論 / 形式理論 / timed-CSP / FDR（失敗-発散-詳細化解析） / FDR（失敗-発散-詳細化）解析 / 国際情報交換（英国、シンガポール） / 国際情報交換（英国、米国）

Outline of Final Research Achievements

The study is concerned with a validity check program for a parallel processing system. If some units are run in parallel, the system will be dead-locked with unexpected sequence failures. We have a tool to find them hidden in a system at the system design level. Our study has tried to refine the validity checker to discover invalidities caused by timing conflict beside simple event sequence. We have confirmed that some of timing invalidities possibly hidden in a system could be found with this newly refined checker.

Research Products

• [Presentation] Native Pythonの並列処理 (2015)
  • Author(s): 福永 力
  • Organizer: 第16回CSP研究会
  • Place of Presentation: 東洋大学（東京都・文京区）
  • Year and Date: 2015-11-21
• [Presentation] ST20プロセッサ -Real Time CSP実現に向けた取り組み (2015)
  • Author(s): 福永 力
  • Organizer: 第15回CSP研究会
  • Place of Presentation: 東洋大学（東京都・文京区）
  • Year and Date: 2015-06-06
• [Presentation] CSPベースの並列処理言語の動向 (2014)
  • Author(s): 福永 力
  • Organizer: 第14回CSP研究会
  • Place of Presentation: 東洋大学・白山キャンパス
  • Year and Date: 2014-11-29
• [Presentation] XMOSのコンテキストスイッチング (2014)
  • Author(s): 福永 力
  • Organizer: 第13回CSP研究会
  • Place of Presentation: 東洋大学・白山キャンパス
  • Year and Date: 2014-05-24
• [Presentation] π-calculusとOccam-π (2013)
  • Author(s): 福永 力
  • Organizer: 第11回CSP研究会
  • Place of Presentation: 東洋大学・白山キャンパス
  • Invited