| 研究課題/領域番号 |
25330008
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 埼玉大学 |
|---|
研究代表者 |
吉浦 紀晃 埼玉大学, 理工学研究科, 准教授 (00302969)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | 仕様記述 / 仕様検証 / 時間論理 / リアクティブシステム / プログラム化可能性 |
|---|
| 研究概要 |
本年度は、リアクティブシステムプログラムの仕様がプログラム化可能であるための必要条件である強充足可能性に関する結果を得た。具体的にはリアクティブシステムプログラムの仕様が強充足可能ではない場合、オートマトンなどのモデルを構築することなく、証明システムつまり式に対して推論規則を適用することにより判定できるかについて、次のことを明らかにした。第一に仕様を記述するための時間論理がNext演算子を含まないUntil演算子のみからなる場合、仕様が強充足可能であるかどうかを証明システムで判定することができないことを証明した。第二に仕様を記述するための時間論理がNext演算子とUntil演算子の両方からなる場合、仕様が強充足可能であるかを証明システムで判定することが可能であることを示した。第三に仕様を記述するための時間論理が「常に成り立つ」を表す演算子のみからなる場合、仕様が強充足可能であるかを証明システムで判定することが可能であることを示した。これらの結果のうち特に、第二の結果から、仕様が強充足可能ではない場合には証明システムだけでは判定できないことが明らかになった。このため、Next演算子とUntil演算子からなる時間論理に対して、強充足可能性や強充足不能性の証明システムの構築を開始している。また、本研究のベースとなっているプログラム化可能性の判定システムの改良や実装上の工夫を加えるなどにより、改良前のシステムでは判定できなかった仕様のプログラム化可能性の判定が可能となった。また、証明システムをどのように利用するかを定める証明戦略を提案した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究はリアクティブシステムプログラムの仕様がプログラム化可能であるかを高速に判定することを目的としている。その高速化の方法としては、プログラム化可能ではない場合にその問題点を見つけ出すことがある。仕様がプログラム化可能ではない原因としてその仕様が強充足不能である場合があり、この性質を判定することで仕様がプログラム化可能ではないことが高速で判定可能となる。今年度の研究実績からNext演算子とUntil演算子の両方からなる証明システムが必要であることが明らかとなり、証明システムの開発を開始している。また、本研究のベースとなるプログラム化可能性の判定システムに対して実装上の工夫を行うことで、これまではプログラム化可能性を判定できなかった仕様を判定可能とすることができるようになるなど、本研究の目的である高速なプログラム化可能性判定システムの開発が確実に進捗しているといえる。また、証明システムをどのように利用するかはプログラム化可能性判定システムの高速化にとっては重要である。今年度の研究実績ではどのように利用するか、つまり証明戦略を構築したので、今後はこの証明戦略の判定システムへの実装を行うことで高速化を行うことできる。以上より、本研究はおおむね順調に進展している。
|
| 今後の研究の推進方策 |
強充足可能性に関する証明システムの開発を進めるとともに、段階的充足可能性についての証明システムの開発を行う。そのために、段階的充足可能性の判定を行うことができる証明システムが構築可能であるかを明らかにする。次に強充足可能性の証明システムの実装を行い、仕様のプログラム化可能性の判定システムに組み込むことで、判定システムの高速化を目指す。さらに、段階的充足可能性の証明システムを構築を行い、さらにその証明システムを実装し、判定システムへ組み込むことでさらに判定システムの高速化を目指す。さらに、今年度の研究実績で得られた証明戦略を判定システムに組み込むことで更なる高速化を目指す。
|
