2004 Fiscal Year Annual Research Report
論理結合子の適切さに基づく有益な情報の導出に関する研究
| Project/Area Number |
15700007
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
吉浦 紀晃 群馬大学, 総合情報処理センター, 助教授 (00302969)
|
|---|
| Keywords | 時間論理 / 仕様記述 / 仕様検証 / リアクティブシステム |
|---|
| Research Abstract |
昨年度に行った論理結合子の適切さの概念の定義を利用目的の1つとして、ソフトウェアやシステム仕様の検証がある。本年度は、世の中の様々な場面で利用されているシステムとして、リアクティブシステムの仕様に対する検証手続きや修正方法、そして、使用からのプログラム合成の方法についての提案を行った。論理結合子の適切さは、これらの形式的手法へ応用することにより、形式的方法では検出できないような仕様の不備を指摘することが可能となる。
本年度は、リアクティブシステムシステム仕様の性質の1つである段階的充足可能性の判定手続きを構築し、その完全性と健全性を証明した。この性質に関してはこれまでに判定手続きが示されていたが、その手続きに誤りがあること、誤りのない手続きを提案した。また、リアクティブシステム仕様に欠陥がある場合の検出方法と、それを修正するための方法を提案した。この検出はタブロー法に基づいており、また、修正方法については、自動的に仕様修正の候補をいくつか示す機能を持っている。リアクティブシステム仕様からのプログラム合成の方法では、プログラムに欠陥があってもプロトタイプを生成することが可能となっており、実際に生成されたプログラムを見て仕様の欠陥を修正することが可能となる。また、生成されるプログラムは複数個考えられるので、何種類かの方針を選んで、プログラムを合成することが可能となっている。
これらの方法は、いずれも形式的な意味論などに基づいて行われているので、仕様が仕様記述者の意図通りに記述されているならば、プログラムの問題点の抽出や修正、また、プログラム合成も有効である。よって、今後は、仕様記述者の意図通り仕様が記述されているかを検証する方法が重要となる。
|
