2015 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 |
プロセス代数ベースの計算モデルについて、Isabelle/HOLなどの定理証明システムを用いて形式化するための研究を推進した。定理証明システムによる形式化は、故障に関する形式的仕様記述を行う上で、基盤技術となる。さらに、最近、定理証明システムはSATなどの推論エンジンを搭載しており、モデル検査システムで行うような網羅的探索を用いることが可能となっている。このことをふまえて、モデル検査における手法と定理証明システムを用いた形式化を統合するような検証手法についても研究を推進してきた。
さらに、このように研究する故障解析の形式的手法を、従来のFMEA（故障モードとその影響解析）やFTA（フォールトツリー解析）などの信頼性工学における手法に対して、どのように形式化し、従来の形式的手法と融合していくことができるのかという点について、研究に着手した。
また、リモート手続き呼び出しやリモートメソッド呼び出しのような分散計算において、故障の概念を形式的に取り扱うための数学的モデルについても、研究を推進した。具体的には、ラムダ計算など、記号論的に計算の概念を取り扱うことができる数学的モデルに対してリモート手続き呼び出しやリモートメソッド呼び出しの計算機構を追加・拡張したものを検討してきた。
|
| 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 |
国際会議発表のための学会登録費・旅費、国際学術論文誌における掲載料や英文校正費用などとして使用予定である。
|
