2015 Fiscal Year Annual Research Report
Timed CSPを用いた実時間並列システム検証プログラムの開発
| Project/Area Number |
25330087
|
|---|
| Research Institution | Tokyo Metropolitan University |
|---|
Principal Investigator |
福永 力 首都大学東京, 理工学研究科, 教授 (00189961)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 並列システム記述理論 / 形式理論 / timed-CSP / FDR（失敗-発散-詳細化解析） |
|---|
| Outline of Annual Research Achievements |
時間概念を取り込んだCSPによる並列処理システムの失敗-発散-詳細化解析プログラムの作成が本研究の具体的課題である．1年目はCSPと同様な並列処理記述理論であるπ-calculusの動向を詳細に調べ、CSPに欠けているπ-calculusのプロセス記述についてそのCSPへの拡張可能性について調べた．
2年目はCSP理論がハードウェア、ソフトウェアとして実現されている例を詳細に調べた．ハードウェアの例ではXMOSであり、ソフトウェアではoccam-pi、またそれを発展させるGuppy計画、XMOS上でのSireコンパイラである．XMOSは現在CSP理論を実装化したFPGAのようなハードウェアチップでその回路記述はCSP理論をもと行われる．またST20というハードウェアもその実現は20世紀の終わりではあるが、CSP理論をもとにリアルタイムカーネルを実装するなど、興味深いCSPのの実現例である．我々はその詳細を検討し、組込みシステムやリアルタイムOS上での安全な並列処理システムの実現にはやはり時間概念を組込んだtimed-CSPの必要性を再確認した．
3年目にその2年間で収集した例をもとにどのような形で失敗-発散-詳細化解析を行うえばもっとも並列システムの安全性（失敗がなく（プロセスの軌跡が追えて）かつ発散のない（デッドタイム、ライブタイムのない）プロセス並列処理）の検討に入ったのだが、同種のプログラムでオックスフォード大学のFDR3は時間概念を取り入れた、しかしあくまでno-timed CSPベースでありながら、時間概念をある程度含むプロセス記述機能の拡張（しかし）に成功し、シンガポール大学のPATは一部時間概念を取り入れたCSPの検証を完成させた．そういった状況で現在CSPそのものの発展と拡張の可能性を確認したところで本研究はそれらの詳細を調べ、どのように我々のtimed CSPを発展させるか新たな曲面に入ったところである．
|
