形式的仕様記述ソフトウェアのエラー特定装置

発明者：
出願人/特許権者：
代理人 (1件)：木村高久
公報種別：公開公報
出願番号（国際出願番号）：特願平4-297341
公開番号（公開出願番号）：特開平6-149560
出願日： 1992年11月06日
公開日（公表日）： 1994年05月27日
要約：

【要約】【目的】形式的仕様記述ソフトウェアの誤りの原因が検出された場合に、この原因の範囲の特定を行うことができる。【構成】検証の対象となる代数的仕様と検証項目とを入力部1から潜在帰納法検証部2に入力すると、潜在帰納法検証部2は、潜在帰納法による代数的検証手続きを行って検証結果を矛盾検出部3に出力するとともに、検証手続きにより生成された等式と簡約された等式および生成に用いられた2つの等式を検証履歴として検証履歴記憶部4に記憶し、矛盾検出部3、検証結果から代数的仕様に誤りがあるか否かを判定し、この結果を逆検証部5に出力する。そして、逆検証部5は、対象となる代数的仕様記述と、検証履歴記憶部4に記憶されている検証履歴および矛盾検出部3による判定結果とから代数的仕様の誤りを逆検証して代数的仕様の誤っていた範囲を等式の修正情報として出力する。

請求項（抜粋）：

形式的仕様と検証項目とから所定の形式的検証手続きにより形式的仕様の検証を行う形式的検証手段を有した形式的仕様記述ソフトウェアのエラー特定装置において、前記形式的検証手段が出力した検証結果から前記形式的仕様に誤りがあるか否かを判定する検証結果判定手段と、前記形式的検証手段の検証履歴を検証情報として記憶する検証情報記憶手段と、前記形式的仕様と前記検証結果判定手段による判定結果および前記検証情報記憶手段に記憶されている検証情報とから逆検証を行い、前記形式的仕様の誤りに関連する箇所を修正情報として出力する逆検証手段とを具備したことを特徴とする形式的仕様記述ソフトウェアのエラー特定装置。

前のページに戻る