2014 Fiscal Year Research-status Report
Ａｍｂｉｅｎｔ Ｃａｌｃｕｌｓの拡張とそれに基づく物流監視システムの構築
| Project/Area Number |
25330095
|
|---|
| Research Institution | Kinki University |
|---|
Principal Investigator |
樋口 昌宏 近畿大学, 理工学部, 教授 (00238289)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | プロセス代数 / モデル検査 / 物流監視 / 時間的性質 |
|---|
| Outline of Annual Research Achievements |
本年度は(1)時間付き多重Ambient Calculusの定義と等価性の検討、(2)時間付きAmbient Calculus のモデル検査に関する検討を予定していた。
(1)については、多重Ambient Calculus、時間付きAmbient Calculusによる物流システムのより望ましいと思われる記述スタイルを継承することに主眼をおいて再検討を行った。その過程で通信プリミティブの取り扱いについていくつかの異なる定義を考案し、現状ではそれらの特質を比較している段階にとどまっている。(2)については時間付きAmbient logicの定義、基本的なモデル検査プログラムの実装、およびいくつかの例題を用いた検証実験まで進めることができた。
予定した項目の他に、時間付きAmbient Calculusによるプロセス式の記述スタイルに物流システムとして「妥当」であるための制約を考案した。そして、記述されたプロセス式がその制約を満たしていることを確認するシステム、あるいはその制約を満たすようなプロセス式の記述を誘導するシステムの試作作業を進めた。
全体として、本来の目的である時間付き多重Ambient Calculusの定義に関連した検討は当初の予定よりかなり遅れているものの、それに関連した諸課題を見いだすことができ、その一部については有力と思われる解決策を与えることができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
研究実績の概要に記した通り、26年度の予定の項目(1)については十分な成果が得られるに至っていない。
当初、本研究では時間付き多重Ambient Calculusの言語仕様を早い時期に策定し、策定した言語による物流記述、ならびにモデル検査に関する研究を進める予定であった。しかしながら、その検討進める過程でベースとなる時間付きAmbient Calculusによる物流システムの記述にいくつかの制約を課すことにより、物流監視システムの構築がより自然に行え、またモデル検査がより効率的に行えることが明らかになってきた。結局26年度は、そのような制約の検討に時間を要し、成果を十分に学会発表、論文投稿の形にまとめることができなかった。
|
| Strategy for Future Research Activity |
次年度は時間付きAmbient Calculusのモデル検査の効率化、ならびに時間付き多重Ambient Calculusの言語の定義と記述性の評価を進める予定である。これにより本研究課題の目的である物流記述のためのAmbient Calculusの拡張が達成できるものと考える。
|
| Causes of Carryover |
今年度は当初の予定になかった時間付きAmbient Calculus による物流記述に課すべき制約の検討に時間を要し、研究成果を発表する機会を十分に持つことができず、当初予定していた学会発表旅費、論文別刷代に支出することができなかった。
|
| Expenditure Plan for Carryover Budget |
次年度は時間付きAmbient Calculusのモデル検査、および時間付き多重Ambient Calculusの定義とそれを用いた物流記述に課すべき制約の検討に注力し、学会発表並びに論文投稿を積極的に進める。特に時間付きAmbient Calculus のモデル検査については、検査プログラムの開発は一部アルバイトを雇用することを想定しており、今年度生じた次年度使用額を有効に活用できるものと考えている。
|
