研究課題/領域番号 |
16K00010
|
研究機関 | 埼玉大学 |
研究代表者 |
吉浦 紀晃 埼玉大学, 情報メディア基盤センター, 准教授 (00302969)
|
研究期間 (年度) |
2016-04-01 – 2019-03-31
|
キーワード | リアクティブシステム / 時間論理 / Coq / OpenFlow |
研究実績の概要 |
時間論理で記述されたリアクティブシステムの仕様の構造、つまり、論理式の形によって、実現可能性に関する各性質の関係が変化することを明らかにした。具体的には、論理式の形によっては、実現可能性と強充足可能性が同一に成る場合、実現可能性と段階的充足可能性が同一に成る場合があることを明らかとなった。この性質を利用することにより、仕様の実現可能性を判定するときに、仕様の形から、実現可能性と強充足可能性や段階的充足可能性が同一になるかを判定し、この結果に基づき、強充足可能性や段階的充足可能性の判定によって、実現可能性の判定を行うことが可能となり、高速に実現可能性の判定を行うことができるようになる。 また、ネットワークをソフトウェアにより構築するSoftware Defined Network (SDN)の一つにOpen Flowがある。OpenFlowは実際にGoogleでのネットワーク構築で利用されている。ネットワークを構築するソフトウェアの検証方法にはモデルチェッキングなどの方法があるが、Coqを利用した検証方法も提案されている。Coqは定理証明を行うシステムであり、この定理証明システムを利用することで、OpenFlowプログラムの検証が可能である。従来の研究では、Coqを利用した検証方法では、ネットワーク機器が単一のみの場合の検証が可能であるが、本研究では、複数のネットワーク機器でも検証可能となる検証方法を提案した。この検証方法を利用することで、ネットワークトポロジーを与えるだけで、基本的なOpenFlowプログラムを構成することができる。
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
理由としては、以下が挙げられる。 時間論理で記述されたリアクティブシステムの仕様の構造と、実現可能性に関する各性質の関係を明らかにすることにより、実現可能性の判定が高速に行える方法を提案できた。つまり、実現可能性の判定よりも計算量が少ない強充足可能性や段階的充足可能性の判定で、実現可能性が判定できる可能性があることが明らかとなった。 また、ネットワークをソフトウェアにより構築するSoftware Defined Network (SDN)の一つであるOpenFlowソフトウェアの検証を定理証明システムであるCoqにより行うことができることを明らかにした。特に、従来の研究では、Coqを利用した検証方法では、ネットワーク機器が単一のみの場合の検証が可能であるが、複数のネットワーク機器でも検証可能となる検証が可能となった。
|
今後の研究の推進方策 |
時間論理で記述されたリアクティブシステムの仕様の実現可能性に関する性質である強充足可能性や段階的充足可能性を判定するための証明システムの証明力の強化、そして、証明システムの完全性と健全性の証明を目指す。 また、OpenFlowネットワークプログラムのCoqによる証明の高速化と、OpenFlowネットワークプログラムの自動合成を目指す。
|
次年度使用額が生じた理由 |
本年度は、時間論理で記述されたリアクティブシステムの仕様の構文と実現可能性の性質の関係を分析し、さらに、CoqによるOpenFlowネットワークプログラムの検証方法の提案をするなど成果を得られたが国際会議等での発表の機会がなかった。このため、旅費を予定していた金額利用することがなかった。
|
次年度使用額の使用計画 |
次年度は、今年度発表できなかった研究成果を国際会議等で発表するために利用する。
|