2015 Fiscal Year Research-status Report
時間論理によるリアクティブシステム仕様のプログラム化可能性の判定とプログラム合成
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 |
本年度は、時間論理で記述されたリアクティブシステムプログラム仕様から、その仕様に含まれる仕様の情報を効率的に導出するための証明システムを実装した。その証明システムはrelevant logicをベースとしている。仕様がプログラム化不能である場合、仕様記述者が仕様を修正する必要があるが、この証明システムは、仕様に含まれる誤りの発見を支援することが可能である。この証明システムに関する成果は国際会議において発表済みである。 次に、リアクティブシステム仕様がプログラム化可能であることの必要条件として段階的充足可能性がある。この性質の判定方法は既に実装済みであるが、実装上の工夫や改良を行うことで高速化を行った。この成果は国際会議で発表済みである。さらに、この実装に対して、証明戦略の導入とその実装を行っており、さらなる高速化が期待できる。 さらに、リアクティブシステム仕様がプログラム化可能であることの必要条件として強充足可能性があり、強充足不能な仕様を強充足可能に修正することは重要である。そこで、仕様の修正方法を提案した。具体的には、リアクティブシステム利用者の動作に対する制限を仕様に加えることにより仕様を修正する。この方法は国際会議において発表済みであり、現在は、この方法の証明システムへの実装を行っている段階である。 また、ネットワーク技術として注目を集めているOpenFlowに対して、本研究により提案された証明システムを提供するために、現在提案されているOpenFlowに対する検証手法の調査分析を行い、現状の検証手法の問題点を見つけ出した。本研究で提案している証明システムによりこの問題点を解決する方法を検討している。この成果は、国際会議での発表が採択されている。
|
Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
本研究の進捗が当初の予定よりも遅く、平成27年度において、本研究の目標である証明システムの実装が十分ではない。現在、証明システムの基本部分の開発はできている。また、証明システムの高速化や開発のための理論的な方法は確立している。しかし、予定している改良の実装が終了していない。また、リアクティブシステムの実現可能性に関連するいくつかの性質の判定方法の実装も終了していない。平成28年度はこれらの実装の完成を目指す。
|
Strategy for Future Research Activity |
これまでに提案した強充足可能性の高速な判定手続き、段階的充足可能性の判定手続きなどを実装することで、リアクティブシステムの実現可能性に関する性質を判定するシステムの実装とさらなる高速化、そして、リアクティブシステム仕様がプログラム化可能でない場合の修正方法など、これまでの研究に提案してきた理論的な方法を実装し、これらを融合することで、リアクティブシステム仕様のプログラム化可能性の高速判定器の構築を目指す。
|
Causes of Carryover |
本研究ではリアクティブシステム仕様の実現可能性に関連する性質の判定方法の実装を含めた、証明システムの開発を行う。この開発は平成27年度に終了予定であったが、開発が遅れているために、平成28年度中の開発を目指している。よって、平成28年度には、この実装に必要となる機器や消耗品などの購入、そして研究成果発表を行うために、平成27年度に支出予定であったこれらの費用が次年度使用額として生じた。
|
Expenditure Plan for Carryover Budget |
本年度は、システム開発の進捗に合わせて必要となる物品や消耗品の購入、そして研究成果の発表などに次年度使用額を充てる。
|
Research Products
(5 results)