2016 Fiscal Year Research-status Report
| Project/Area Number |
24500009
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
西崎 真也 東京工業大学, 学術国際情報センター, 教授 (90263615)
|
|---|
| Project Period (FY) |
2012-04-01 – 2018-03-31
|
| Keywords | モデル検査 / プロセス計算 / システムの形式化 / 故障 |
|---|
| Outline of Annual Research Achievements |
これまで行ってきたプロセス代数ベースの計算モデルや有限状態オートマトンベースの研究モデルによる、故障時の振る舞いの解析手法に関して取りまとめを行った。
また、故障をとらえる計算モデルの定理証明システム上での形式化を行ってきたが、それについて研究の取り組みを継続してきた。
また、これらの故障解析手法を統合的に扱う検証システムについて設計を行ってきた。
これらの他に、故障の解析技術を拡張するような取り組みについてもおこなった。
具体的には、Webシステムのパフォーマンスに関する解析を、モデル検査技法を応用して、実システムに近い形で可能とする手法である。ＷｅｂシステムのフレームワークにＳＭＴソルバーに入力可能な形式となる制約を抽出する。その制約を解消することにより、構築したＷｅｂサーバーアプリケーションのパフォーマンス解析を可能とする。抽出した制約にさらに事前に測定した実際の実行時間情報を加えることにより、より現実の実行時間に近い形で、パフォーマンス解析が可能となっている。このようなパフォーマンス解析は、故障解析につながるものとして期待できる。
それに加えて、さらに関数型言語における遅延評価の一種である名前呼び評価のための分散・並列計算モデルの形式化についても取り組んだ。計算モデルは、操作的意味論により構築したものであり、ラムダ計算をＲＰＣの仕組みを組み込んだものとなる。故障解析の対象となるシステムは、分散性や並列性を有するものが多い。したがって、分散・並列計算モデルの研究は重要となる。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究課題を順調に進行することに成功し、学術上の研究成果についても着実にあげている。具体的には、故障の解析技術を拡張するような取り組みについてもおこなった。
具体的には、Webシステムのパフォーマンスに関する解析を、モデル検査技法を応用して、実システムに近い形で可能とする手法を提案した他、関数型言語における遅延評価の一種である名前呼び評価のための分散・並列計算モデルの形式化についても取り組んだ。
|
| Strategy for Future Research Activity |
これまで取り組んできた研究成果について、整理を行い、それらの研究成果を公表していく。また、個々の研究成果について相互関係を明確にして、全体的な総括をおこなっていくことを予定している。
|
| Causes of Carryover |
平成２８年度において行う予定の研究成果の発表予定が、勤務する大学における配置換えおよび昇任に伴う業務のため、平成29年度に変更することになったため。
|
| Expenditure Plan for Carryover Budget |
研究成果を国際会議発表するための旅費、国際論文誌に投稿に伴う英文校正費用、そして、論文誌における掲載料などに充てることを予定している。
|
