研究課題/領域番号 |
25330008
|
研究種目 |
基盤研究(C)
|
配分区分 | 基金 |
応募区分 | 一般 |
研究分野 |
情報学基礎理論
|
研究機関 | 埼玉大学 |
研究代表者 |
吉浦 紀晃 埼玉大学, 情報メディア基盤センター, 准教授 (00302969)
|
研究期間 (年度) |
2013-04-01 – 2017-03-31
|
研究課題ステータス |
完了 (2016年度)
|
配分額 *注記 |
4,810千円 (直接経費: 3,700千円、間接経費: 1,110千円)
2015年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2014年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円)
2013年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
キーワード | 時間論理 / モデルチェッキング / 実現可能性 / リアクティブシステム / 適切さの論理 / 仕様記述 / プログラム化可能性 / 仕様検証 |
研究成果の概要 |
本研究の成果は、時間論理で記述されたリアクティブシステムの仕様の実現可能性を、推論規則とオートマトンを利用した判定システムにより高速に判定することが可能となり、特に実現可能ではない場合の判定が高速化された。さらに、実現可能ではない仕様を、実現可能に修正するための修正方法として、要求制約式の新たな導出方法を提案した。これにより実現可能な仕様への修正を支援することが可能となった。さらに、仕様から有益な情報を推論するシステムの高速化を行った。 さらに、ネットワークをソフトウェアにより構築する方法であるOpenFlowのネットワークをネットワークトポロジーから構成するための基盤となる検証方法を構築した。
|