2005 Fiscal Year Annual Research Report
論理結合子の適切さに基づく有益な情報の導出に関する研究
| Project/Area Number |
15700007
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
吉浦 紀晃 群馬大学, 総合情報メディアセンター, 助教授 (00302969)
|
|---|
| Keywords | 時間論理 / 仕様記述 / 仕様検証 / リアクティブシステム / システム検証 / プログラム合成 |
|---|
| Research Abstract |
本年度は、リアクティブシステムシステム仕様からプログラムを合成する方法と各種性質を判定する方法の提案を行い、その方法の正当性の証明を行った。このプログラムを合成する方法においては、仕様に含まれる論理結合子の適切さ、具体的には、古典論理における論理結合子である含意、否定、論理和、論理関に関する出現の適切さを利用することにより、合成される可能性のある多くのプログラムから利用者にとって有効であると予想されるプログラムを合成することが可能である。また、プログラムを合成するためには、その仕様からプログラムが合成可能であるかどうかを検証することが必要であるが、そのための検証方法においても仕様に含まれる論理結合子の適切さを考慮することによる検証方法の構築を行った。論理結合子の適切さを考慮することは現時点では、適切さを判定するための計算量などの問題があるため実用的であるとは言い難い。つまり、適切さを考慮せずに仕様のプログラム合成の可能性を判定するほうが効率的である。しかしながら、何らかの工夫を導入することにより判定を高速に行うことが可能であると思われる。また、プログラム合成に関しては、合成に関する方向性が与えられるので、プログラム合成を効率的に行うことが可能となる。しかしながら、からなずしも、最適なプログラムが与えられるわけではないので、改善が必要である。
また、本研究における論理結合子の適切さを利用することにより、移動体通信のシミュレーションプログラムや、防犯カメラシステムなどのシステムの検証を手動で行い、その有効性を確認した。今後は、これらの自動的な検証システムの構築を行うことが重要となる。また、本研究で提案した各種の方法の実装や高速化が今後の課題としてあげられる。
|
