| 研究課題/領域番号 |
25330087
|
|---|
| 研究機関 | 首都大学東京 |
|---|
研究代表者 |
福永 力 首都大学東京, 理工学研究科, 教授 (00189961)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 並列システム記述理論 / 形式理論 / timed-CSP / FDR（失敗-発散-詳細化）解析 / 国際情報交換（英国、シンガポール） |
|---|
| 研究実績の概要 |
時間概念を取り組んだCSPを理論的土台とした並列処理システムの失敗-発散-詳細化解析プログラムの構築が我々の本課題の目標である．そのためには1）（machine-readable）timed-CSPで記述された並列システムのコンパイラの作成、2）そのFDR解析、3）CSP記述の拡張（Mobile-channelあるいは共有メモリ）とそれに応じたコンパイラの拡張、といったステップで研究を進めている．またさまざまな時間概念にクリティカルな並列システムの例の収集も行う．
昨年度はコンパイラの作成に集中しようと考えたがtimed processを含まないnon timedなCSPに関してのコンパイラはすでに存在しておりFDR-2としてモデル検査アプリケーションとしてオックスフォード大学から公表されている．研究・教育目的であればフリーでのその利用が可能である．使用実績もありコンパイラ部の信頼性も高いものである．そこで我々がtimed-CSPとしていくつかの時間概念のCSP文法要素を導入してコンパイラ全体の新生を目指すのではなく（もちろんオックスフォード大学のコンパイラを凌ぐものが出来るのであれば問題ないが）、むしろtimed-CSPの概念を今までのnon-timed CSPで解釈可能なプロセス記述として考案してそれをFDR-2に組み込めないか検討してみた．連続量としての時間の概念を離散化して最小単位の時間単位を導入する．その時間単位の整数倍の遅延はその整数回のdelayイベントの発生の繰り返しで対処する．timed-CSPというところをdelayed-CSPという概念で離散的時間を導入しタイミング記述を行う．そしてdelayのプロセス記述を現状のFDR-2で行うというものである．今その記述の作成にとりかかっているところである．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
まずTimed CSP（CSPとはCommunicating Sequential Processesの略）について、関係各国の取組状況の調査を行った．そしてCSPにtiming概念を入れた並列システムの検証の意義について再度見直し、検証プログラム開発に新規性があることを再確認した．しかし相手とするオックスフォード大学がFDR-2に続くFDR-3を新たな（しかしまだnon-timed CSPだが）並列システム検証システム（検査機）としてリリースさせた．このFDR-3をもってもまだイベント発生の順番と時間のズレに矛盾があればその検証に齟齬が生じる可能性もあるのだが注目すべきはFDR-3でなされたそのプロセス記述能力の拡張である．この新たな拡張機能を使えば項目「研究実績の概要」で述べたdelayプロセスの記述が可能なのではないかというアイデアが浮かんできた．そこで現在は独自の検証システムの開発という方向をややトーンダウンしFDR-3の枠組みで離散時間の概念を導入してtimed CSPプロセスを表現させる方向に転換しているところである．
ところでシンガポール大学がPATという高機能CSP検査機を開発している．シンガポール大学から非営利目的であればその利用が認められている．商用目的では日本の企業がこのライセンスを販売している．このPATも最近リニューアルされてより拡張されたものになっているということが判明した．timed CSPの概念も全てではないが取り込んでいるとの説明もあることがわかった．現在このPATを取り寄せてその詳細を調査しようとしているところである．timed CSPプロセスの検証にはプロセスの表現の検証プログラム内での取り扱いの調整がうまくなされていないと検証時間がプロセスの複雑さ増大とともに爆発的に長くなってしまう可能性がある．PATがtimed-CSP事象の検証をどこまで行えるのか事象に係る状態数と検証時間の関係も追いながら調査していこうと考えている．
|
| 今後の研究の推進方策 |
研究の方向はTimed CSPを用いた並列システムの検証プログラムの開発というところは明確に維持されているがそのアプローチがやや変化したということを前（11）項で述べた通りである．FDR-2がFDR-3となりプロセス記述能力が増強され離散化されたものではあるが時間の経過をイベントとして取り込めるプロセスの記述が可能になった．いままで連続時間であるがTimed CSP特有のコンストラクタはそれをコンパイラに取り込むことでいわば正面突破の形で乗り越えようとしたが必ずしもその必要はなく今の枠組みでTimed CSPイベントを含んだプロセス記述（delay）で乗りきれるようになった．離散時間記述でどこまで本来連続である時間の概念が表現できるかギャップはあるのか慎重に検証する必要があるが、あるいはそのギャップが生ずる例を見出さなければならないがいまは離散時間delayプロセスの確立に向かって研究を進めていこうと思っている．またシンガポール大学のPATの連続時間記述によるTimed CSPプロセスの記述能力について検証し評価を下さなければならない．いくつかの例をdelayプロセスを加えたFDR-3とPATとで性能比較を行い優劣を論じなければならない．またdelayプロセスのその結果を元にした改良にとり組む必要もあるのかもしれない．残された1年であるが今後このdelayプロセスの完成に向けて邁進していこうと考えている．
|
| 次年度使用額が生じた理由 |
物品費の増加は当初計画になかったのだが開発用PCの障害、これが修理不可能となったため新規物品として購入したためである．その他の経費は並列システムの実証実験として導入しているメニーコアシステム（昨年度別途財源で購入）の年間メインテナンス料の支出のためであった．出張には他の財源をあててそれを他の用途に回した．
|
| 次年度使用額の使用計画 |
26年度人件費の支出はほぼ予定通りであった．27年度も人件費支出に関してはその予定でいこうと考えている．前項で記したようにメニーコアシステム使用のメインテナンス経費約25万円の支払いが余分にあるが物品費、旅費のやりくりで工面できると考えている．
|
