本研究の成果は、時間論理で記述されたリアクティブシステムの仕様の実現可能性を、推論規則とオートマトンを利用した判定システムにより高速に判定することが可能となり、特に実現可能ではない場合の判定が高速化された。さらに、実現可能ではない仕様を、実現可能に修正するための修正方法として、要求制約式の新たな導出方法を提案した。これにより実現可能な仕様への修正を支援することが可能となった。さらに、仕様から有益な情報を推論するシステムの高速化を行った。 さらに、ネットワークをソフトウェアにより構築する方法であるOpenFlowのネットワークをネットワークトポロジーから構成するための基盤となる検証方法を構築した。
|