2019 Fiscal Year Annual Research Report
Proof system for Realizability Decision of Reactive System Specification described by Temporal Logic
| Project/Area Number |
16K00010
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
吉浦 紀晃 埼玉大学, 理工学研究科, 教授 (00302969)
|
|---|
| Project Period (FY) |
2016-04-01 – 2020-03-31
|
| Keywords | 時間論理 / OpenFlow / モデル検査 |
|---|
| Outline of Annual Research Achievements |
時間論理により記述されたリアクティブシステムの仕様の性質の分類を構文的に行う方法を構築し、その正当性を証明している状況であるが完成していない。リアクティブシステム仕様の性質はSafety Propertyと Liveness Propertyに分類される。
これら２つの性質を検証する方法が異なるため分類する方法は重要である。それぞれの検証を行うための証明戦略は異なるため、予めいずれの性質であるかを知っていることは検証の効率をあげることになる。特に、これら2つの性質を構文的に性質を分類することが可能になると仕様の長さの多項式時間で分類が可能となり、リアクティブシステム仕様から安全性を満たすリアクティブシステムをプログラム化可能であるかを効率よく判定することができる。よって、プログラム化可能性判定の計算量を減少させることが可能となる。
また、本年度は、ネットワーク機器を制御するためのOpenFlowのソフトウェアの検証をCoqやモデル検査器を用いて行なった。具体的には、CoqによりOpenFlowのソフトウェアのパケット到達可能性を行うと同時に、モデル検査器を用いることで同様の検査を行なった。また、秘密計算に基づく位置情報サービスシステムの構築を行い、そのシステムの検証において時間論理とモデル検査を用いた。これらの実際のシステムの検証から、現実に必要となるシステムの性質を時間論理で記述した場合の式の構造について分析を行い、性質の分類の効率化に利用した。
|
