時相論理による段階的仕様記述プロセスに対応した検証法

概要

論文の詳細を見る
形式的な仕様記述に関する研究が行なわれている。例えば、時相論理によるリアクティブシステムの仕様記述に関する研究がある。その主な目的は、仕様の段階での性質検証である。また一方、仕様記述の計算機支援を行なう研究も行なわれている。多くは、構文エディタやブラウザ等に見られるように、「記述そのもの」に対する支援が主であり、検証のような意味的な支援を記述プロセスと深く関係付けた研究は少ない。現実の仕様記述過程では、まずプロトタイプを記述し何度も修正を行ないつつ目的となるシステムの仕様を完成させる。仕様を修正する度に、記述された仕様に対する検証結果が得られるならば、仕様誤りの早期発見にもつながり、開発時間の短縮につながると考えられる。これを低い計算コストで実現するためには、仕様が修正される過程と密接に関係した検証方法が必要である。修正前後の仕様の差分と前回の検証から、修正後の仕様の検証を行なう方法を実現することが本研究の目的である。論理式で記述された仕様の様々な性質検証の多くは、論理式の無矛盾性の判定、すなわち充足可能性判定に帰着される。充足可能性判定の方法のひとつにタブロー法があるが、この方法が用いるデータ構造は意味グラフであるため理解しやすく、また、データ構造、アルゴリズムが単純なため計算機による支援に適している。[1][2]において、以前の検証に用いたタブローを再利用し効率的なタブロー構成を行なう手続きが示されている。この手続きは、すでに記述されている仕様の中に誤りを発見した際に、その仕様を削除する場合には対応していない。そこで本研究では、より柔軟な仕様の修正方法を考え、仕様を書き加える場合だけでなく誤った仕様を取り除く場合にも、修正前のタブローの再利用が可能なタブローを与える。
一般社団法人情報処理学会の論文
1995-03-15

時相論理による段階的仕様記述プロセスに対応した検証法

スポンサーリンク

概要

著者

関連論文

スポンサーリンク