2018 Fiscal Year Research-status Report
時間論理によるリアクティブシステム仕様のプログラム化可能性判定を行う証明システム
| Project/Area Number |
16K00010
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
吉浦 紀晃 埼玉大学, 大学院理工学研究科, 教授 (00302969)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | リアクティブシステム / 時間論理 / Safety Property / Liveness Property |
|---|
| Outline of Annual Research Achievements |
時間論理により記述されたリアクティブシステムの仕様の性質の分類を構文的に行う方法を構築した。リアクティブシステム仕様の性質はSafety PropertyとLiveness Propertyに分類される。安全性を保障するためにはSafety Propertyが満たされることが重要であるため、仕様からSafety Propertyを分類し、その性質を満たすリアクティブシステムを構築することも有効である。
リアクティブシステム仕様の性質をこの２種類に分類する方法は、リアクティブシステムからモデルを構成してそのモデルを解析することでしか、これまではできなかった。ここでいうモデルは、状態遷移図であり、この構築には仕様の長さの指数オーダが必要である。よって、性質を分類することはリアクティブシステム仕様のプログラム化可能性と同程度の計算量を必要としていた。構文的に性質を分類することが可能になると仕様の長さの多項式時間で分類が可能となり、リアクティブシステム仕様から安全性を満たすリアクティブシステムをプログラム化可能であるかを判定することができる。よって、プログラム化可能性判定の計算量を減少させることが可能となる。
また、昨年度は、モデル検査ツールの一つであるUPPAALを利用して実際のシステム記述を行い自動車ネットワークの一つであるTTCANの検証を行いその有効性を確認したが、今年度は、開発中のネットワーク管理ロボットのプログラムの検証に用いて、モデル検査手法の有効性を確認した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
論理式の制限やモデル化の限定が、モデル検査においては有効であることはわかったが、今年度は仕様の性質をSafety PropertyとLiveness Propertyに構文的に分類することが可能となることがわかった。よって、性質を分類することで、モデル検査に必要とする計算時間を減らすことが可能である。また、プログラム化可能性の判定にも有効であることがわかった。
|
| Strategy for Future Research Activity |
システム仕様を記述する場合に、論理式の制限の実施により、より効率的にプログラム化可能性の判定が行えるかどうか分析する。さらに、システム仕様を記述時のモデルを限定することで、システム仕様のプログラム化可能性の判定が効率化されるかどうか、そして、どの程度の効率化されるかを分析し、システム仕様のプログラム化可能性の高速化を目指す。また、リアクティブシステム仕様をSafety PropertyとLiveness Propertyに分類して、プログラム化可能性を判定する場合に、各性質に特化した効率化が行えるかどうかを調べる。
|
| Causes of Carryover |
研究の進捗がやや遅れているため、成果発表などが実施できていない。よって、成果発表に利用予定の予算が残金として残っている。今年度はこれまでの成果発表を行うため、この残金を利用する予定である。
|
