2014 Fiscal Year Research-status Report
| Project/Area Number |
24500009
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
西崎 真也 東京工業大学, 情報理工学(系)研究科, 准教授 (90263615)
|
|---|
| Project Period (FY) |
2012-04-01 – 2017-03-31
|
| Keywords | モデル検査 / プロセス代数 / システムの形式化 |
|---|
| Outline of Annual Research Achievements |
振る舞いの解析手法に基づき検証システムの開発に着手した。プロセス代数ベースの計算モデル・有限状態オートマトンベースの計算モデルのいずれにおいても、バックエンドの推論システムとして、既存のモデル検査システムを位置づけ、フロントエンドには、前項の成果である計算モデルの変換システムを据えた。
その他に上記のような推論システムの実装の研究の他に、関連する重要な研究として、以下の様なテーマに取り組んだ。
交換機におけるコネクション確立に関する通信プロトコルをプロセス代数ベースの計算もでるのもとで、形式化することができることを示した。この成果は、プロセス代数、特に、メモリ消費に関してセンシティブであるような計算体系であるspice計算の実用性に対して、一定の評価を行うことが可能となった。また、spice計算に対して、実際上の使用を行うに際して、どのような機能拡張や機能調整が必要であるのかということにおいて、重要な知見をえることができた。
その他にCPUの速度に依存するような組み込みシステムにおいて、システムの動作のCPU速度依存性をモデル計算システムを用いて、解析することに一定の成功を納めた。これにより、本研究における「推論バックエンドとしてのモデル検査システム」の有効性に道筋をつけることができた。また、実際のシステムを形式的に記述するということにおいて、様々な知見を得ることができ、来年度以降の本研究に重要な貢献となった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究課題を遂行するにあたって重要となるテーマや視点を発見することができ、また、学術上の研究成果を得ることができた。
|
| Strategy for Future Research Activity |
研究計画に沿って、本研究課題を遂行していく。また、随時、研究計画の検討を行い、研究の円滑な推進を目指していくこととしている。
|
| Causes of Carryover |
本年度研究成果の発表が、来年度においての国際会議での発表となり、その経費を来年度に計上するため。
|
| Expenditure Plan for Carryover Budget |
研究成果の発表のための国際会議発表に関わる旅費、および、発表論文原稿の英文校正など、国際会議発表に関連する経費として使用する予定である。
|
