2017 Fiscal Year Research-status Report
時間論理によるリアクティブシステム仕様のプログラム化可能性判定を行う証明システム
| Project/Area Number |
16K00010
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
吉浦 紀晃 埼玉大学, 情報メディア基盤センター, 准教授 (00302969)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | リアクティブシステム / 時間論理 / モデル検査 |
|---|
| Outline of Annual Research Achievements |
時間論理により記述されたリアクティフシステムの仕様の構造、つまり、論理式の形が限定されている場合について、リアクティブシステムの仕様のプログラム可能性の判定が容易になることが前年度の研究で明らかとなった。今年度は、この制限がモデル検査の場合に有効であるか、また、実際のプログラム化可能性の判定を行うための仕様を用意するために、実際のシステムの仕様記述を行なった。つまり、様々なシステムの仕様を記述して、実際に、本研究で開発予定のプログラム化可能性の判定システムの実験を行うための準備を行なった。
さらに、この仕様記述の１つを実際のモデル検査ツールであるUPPAALを利用して実際のシステム記述を行った。UPPAALでは、システム仕様をCTLのサブセットで記述することから、論理式の形が制限されている。この場合のモデル検査における実用性について調べた。その結果、構文が限定されていたとしても、モデルの大きさに依存して、処理時間が大きくなること、そして、対象となるシステムのモデル化の仕方によって、処理時間が大きく変化することがわかった。よって、構文の制限に加えて、モデル化の仕方が処理時間に影響を与えることがわかった。論理式の形の制限に加え、モデル化についても制限を行うことが必要であることがわかった。
今年度の研究から、システム仕様を記述する際にも、論理式の形の制限が有効であるだけでなく、システム仕様を記述する際のモデル化の制限も重要であると予想される。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
論理式の制限やモデル化の限定が、モデル検査においては有効である、つまり、モデル検査に必要とする計算時間を減らすことに有効であることがわかった。しかし、論理式の制限やモデル化の制限が、本研究の目標であるシステム仕様のプログラム化可能性判定が高速化に有効であるかは明らかではない。よって、モデル検査における結果を利用して、プログラム化可能性の判定の高速化を目指す必要があるが、この高速化で遅れが生じている。
|
| Strategy for Future Research Activity |
システム仕様を記述する場合に、論理式の制限の実施により、より効率的にプログラム化可能性の判定が行えるかどうかを分析する。さらに、システム仕様を記述時のモデルを限定することで、システム仕様のプログラム化可能性の判定が効率化されるかどうか、そして、どの程度の効率化されるかを分析し、システム仕様のプログラム化可能性の高速化を目指す。
|
| Causes of Carryover |
(理由)
本年度は、時間論理で記述されたリアクティフシステムの仕様の構文とモデル検査における効率化の関係を分析し、構文の制限がある場合、モデル検査では実用的な時間での利用が可能であることがわかった。以上の成果が得られたが国際会議等での発表の機会がなかった。このため、旅費を予定していた金額利用することができなかった。また、本年度は、高性能計算機を購入したが、さらなる計算機の購入までは研究が進まなかった。
(使用計画)
次年度は、今年度発表できなかった研究成果を国際会議等で発表するために利用する。また、研究の進捗に合わせ、必要となる計算機の購入を行う。
|
