特許

J-GLOBAL ID：200903050231028539

プロパティ検証方法および装置

発明者： 中田 恒夫 ,  岩下 洋哲
出願人/特許権者： 富士通株式会社
代理人 (1件)： 古谷 史旺 (外1名)
公報種別：公開公報
出願番号（国際出願番号）：特願平8-220005
公開番号（公開出願番号）：特開平10-063537
出願日： 1996年08月21日
公開日（公表日）： 1998年03月06日
要約：

【要約】【課題】 記号モデル検査法において、メモリ規模の縮小と処理時間の短縮とを両立可能なプロパティ検証方法および装置を提供する。【解決手段】 同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証するプロパティ検証方法において、検証対象のプロパティとして、枝分かれのない一本の状態集合列あるいは枝分かれのない一本の状態集合列に無限ループが連結した構成の状態集合列を示す単一パス表現が入力され、単一パス表現を有限状態機械における像計算処理のみで実行可能な所定の手続きを順次に組合せた手続き列に変換し、手続き列で示された各手続きを実行して、単一パス表現に対応する状態遷移のパスを経由する状態集合を求め、得られた状態集合が空集合であるか否かに基づいて、実例発見あるいは実例なしを通知する。

請求項（抜粋）：

同期式順序機械の動作を表す有限状態機械が、機能仕様を表すプロパティを満たしているか否かを検証するプロパティ検証方法において、検証対象のプロパティとして、枝分かれのない一本の状態集合列あるいは枝分かれのない一本の状態集合列に無限ループが連結した構成の状態集合列を示す単一パス表現が入力され、前記単一パス表現を前記有限状態機械における像計算処理のみで実行可能な所定の手続きを順次に組合せた手続き列に変換し、前記手続き列で示された各手続きを実行して、前記単一パス表現に対応する状態遷移のパスを経由する状態集合を求め、得られた状態集合が空集合であるか否かに基づいて、実例発見あるいは実例なしを通知することを特徴とするプロパティ検証方法。

IPC (2件)：

G06F 11/28 340 ,  G06F 17/50

FI (2件)：

G06F 11/28 340 A ,  G06F 15/60 664 G

引用特許：

審査官引用 (1件)

• ハイブリッドモデル状態マシーンにおける到達可能状態を決定するための方法及び装置
  公報種別：公開公報   出願番号：特願平7-138355   出願人：エイ・ティ・アンド・ティ・コーポレーション