2016 Fiscal Year Annual Research Report
Realizability Decision and Program Synthesis for Reactive System Specification described by Temporal Logic
| Project/Area Number |
25330008
|
|---|
| Research Institution | Saitama University |
|---|
Principal Investigator |
吉浦 紀晃 埼玉大学, 情報メディア基盤センター, 准教授 (00302969)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 時間論理 / モデルチェッキング / 実現可能性 / リアクティブシステム / 適切さの論理 |
|---|
| Outline of Annual Research Achievements |
平成２８年度は、平成２７年度に研究発表を行った、時間論理により記述されたリアクティブシステムの仕様の実現可能性の性質の一つである段階的充足可能性や強充足充足可能性の判定手続きを、本格的に実装を開始した。さらに、これら２つの判定手続きを統合することで、実現可能性の判定手続きを構築した。実装は進んでおり、この判定手続きは段階的充足可能性や強充足可能性をより高速に判定できる。しかし、改良の必要な部分がまだまだ多く、改良を継続している段階である。
さらに、実現可能性の判定手続きの高速化を行うために、時間論理で記述された仕様の構造、具体的には、構文の構造と実現可能性の関係を明らかにすることを目指した。その結果、論理式の形によって、実現可能性と強充足可能性や段階的充足可能性が一致する場合があることを明らかにした。これを利用することで、実現可能性の判定を強充足可能性や段階的充足可能性の判定に還元することで、実現可能性の判定が高速となる。
また、ネットワークをソフトウェアを利用して構成するSoftware Defined Network(SDN)の一つであるOpenFlowのプログラミング言語であるNetCoreを利用した検証ツールの拡張を行った。具体的には、従来のNetCoreでは検証できなかったループの検出などを行う方法を提案し、実際に、検出を行うことが可能であることを示した。初期の段階では、検証するための命題を手作業で作成する必要があったが、命題の生成を自動化することで、検証の自動化を行うことができた。この検証の自動化を利用することで、NetCoreによるプログラムを、ネットワークトポロジーから自動的に生成することが可能となる。
|
