2013 Fiscal Year Research-status Report
| Project/Area Number |
24500009
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
西崎 真也 東京工業大学, 情報理工学(系)研究科, 准教授 (90263615)
|
|---|
| Keywords | 故障 / 計算モデル |
|---|
| Research Abstract |
前年度において確立した二種類の計算モデルに対して振る舞いの解析手法の提案を行った。これは前年度の意味論に関する研究の延長線上に位置する課題となっている。
【プロセス代数ベースの計算モデル】pi計算やACPを拡張した得られた計算モデルから、従来のpi計算・ACPなどのプロセス代数への変換を与えた。そして、変換を通じて意味が保存されること、すなわち、プロセス式の振る舞いが保存されることを示した。そして、変換先でのモデルに対する言明を変換元の言明として解釈する手法について研究した。
【有限状態オートマトンベースの計算モデル】
前年度に研究した、故障をとらえた計算モデルから通常の有限状態オートマトンへの変換について研究を進めた。特に、変換先で成り立つ時相論理式を変換元の時相論理式として解釈する方法について研究を行った。
|
| 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 |
平成２５年度に引き続き、得られた成果についての洗練について取り組む他、振る舞いの解析手法に基づき検証システムの開発をおこなう予定である。プロセス代数ベースの計算モデル・有限状態オートマトンベースの計算モデルのいずれにおいても、バックエンドの推論システムとして、既存のモデル検査システムを位置づけ、フロントエンドには、前項の成果である計算モデルの変換システムを据えることを企画している。
|
| Expenditure Plans for the Next FY Research Funding |
国際会議への論文発表および学術雑誌への掲載が、次年度に行われることとなり、それに充てるように計画した経費を次年度の使用額とするため。
国際会議での論文発表にともなう、旅費、国際会議登録費、英文校正費用に充てる他、学術雑誌への掲載においては、論文掲載費、英文校正費用等に充てる予定である。
|
