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

• Item type: National Convention(1)
• 公開日: 1995-03-15
• タイトル: 時相論理による段階的仕様記述プロセスに対応した検証法
• タイトル / 言語: en
• タイトル: Stepwise Verification of Specifications in Temporal Logic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 東京工業大学 情報理工学研究科 計算工学専攻
• 著者所属: 東京工業大学 情報理工学研究科 計算工学専攻
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute of Technology
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Engineering, Tokyo Institute of Technology
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 形式的な仕様記述に関する研究が行なわれている。例えば、時相論理によるリアクティブシステムの仕様記述に関する研究がある。その主な目的は、仕様の段階での性質検証である。また一方、仕様記述の計算機支援を行なう研究も行なわれている。多くは、構文エディタやブラウザ等に見られるように、「記述そのもの」に対する支援が主であり、検証のような意味的な支援を記述プロセスと深く関係付けた研究は少ない。現実の仕様記述過程では、まずプロトタイプを記述し何度も修正を行ないつつ目的となるシステムの仕様を完成させる。仕様を修正する度に、記述された仕様に対する検証結果が得られるならば、仕様誤りの早期発見にもつながり、開発時間の短縮につながると考えられる。これを低い計算コストで実現するためには、仕様が修正される過程と密接に関係した検証方法が必要である。修正前後の仕様の差分と前回の検証から、修正後の仕様の検証を行なう方法を実現することが本研究の目的である。論理式で記述された仕様の様々な性質検証の多くは、論理式の無矛盾性の判定、すなわち充足可能性判定に帰着される。充足可能性判定の方法のひとつにタブロー法があるが、この方法が用いるデータ構造は意味グラフであるため理解しやすく、また、データ構造、アルゴリズムが単純なため計算機による支援に適している。[1][2]において、以前の検証に用いたタブローを再利用し効率的なタブロー構成を行なう手続きが示されている。この手続きは、すでに記述されている仕様の中に誤りを発見した際に、その仕様を削除する場合には対応していない。そこで本研究では、より柔軟な仕様の修正方法を考え、仕様を書き加える場合だけでなく誤った仕様を取り除く場合にも、修正前のタブローの再利用が可能なタブローを与える。
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00349328
• 書誌情報: 全国大会講演論文集; 巻 第50回, 号 ソフトウェア, p. 305-306, 発行日 1995-03-15
• 出版者 / 言語: ja
• 出版者: 情報処理学会