研究課題/領域番号 |
16K00010
|
研究機関 | 埼玉大学 |
研究代表者 |
吉浦 紀晃 埼玉大学, 大学院理工学研究科, 教授 (00302969)
|
研究期間 (年度) |
2016-04-01 – 2020-03-31
|
キーワード | リアクティブシステム / 時間論理 / Safety Property / Liveness Property |
研究実績の概要 |
時間論理により記述されたリアクティブシステムの仕様の性質の分類を構文的に行う方法を構築した。リアクティブシステム仕様の性質はSafety PropertyとLiveness Propertyに分類される。安全性を保障するためにはSafety Propertyが満たされることが重要であるため、仕様からSafety Propertyを分類し、その性質を満たすリアクティブシステムを構築することも有効である。 リアクティブシステム仕様の性質をこの2種類に分類する方法は、リアクティブシステムからモデルを構成してそのモデルを解析することでしか、これまではできなかった。ここでいうモデルは、状態遷移図であり、この構築には仕様の長さの指数オーダが必要である。よって、性質を分類することはリアクティブシステム仕様のプログラム化可能性と同程度の計算量を必要としていた。構文的に性質を分類することが可能になると仕様の長さの多項式時間で分類が可能となり、リアクティブシステム仕様から安全性を満たすリアクティブシステムをプログラム化可能であるかを判定することができる。よって、プログラム化可能性判定の計算量を減少させることが可能となる。 また、昨年度は、モデル検査ツールの一つであるUPPAALを利用して実際のシステム記述を行い自動車ネットワークの一つであるTTCANの検証を行いその有効性を確認したが、今年度は、開発中のネットワーク管理ロボットのプログラムの検証に用いて、モデル検査手法の有効性を確認した。
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
論理式の制限やモデル化の限定が、モデル検査においては有効であることはわかったが、今年度は仕様の性質をSafety PropertyとLiveness Propertyに構文的に分類することが可能となることがわかった。よって、性質を分類することで、モデル検査に必要とする計算時間を減らすことが可能である。また、プログラム化可能性の判定にも有効であることがわかった。
|
今後の研究の推進方策 |
システム仕様を記述する場合に、論理式の制限の実施により、より効率的にプログラム化可能性の判定が行えるかどうか分析する。さらに、システム仕様を記述時のモデルを限定することで、システム仕様のプログラム化可能性の判定が効率化されるかどうか、そして、どの程度の効率化されるかを分析し、システム仕様のプログラム化可能性の高速化を目指す。また、リアクティブシステム仕様をSafety PropertyとLiveness Propertyに分類して、プログラム化可能性を判定する場合に、各性質に特化した効率化が行えるかどうかを調べる。
|
次年度使用額が生じた理由 |
研究の進捗がやや遅れているため、成果発表などが実施できていない。よって、成果発表に利用予定の予算が残金として残っている。今年度はこれまでの成果発表を行うため、この残金を利用する予定である。
|