特許

J-GLOBAL ID：200903007914928672

論理装置の検証データ生成方法

発明者： 中田 恒夫 ,  岩下 洋哲 ,  広瀬 文保
出願人/特許権者： 富士通株式会社
代理人 (1件)： 竹内 進 (外1名)
公報種別：公開公報
出願番号（国際出願番号）：特願平8-037640
公開番号（公開出願番号）：特開平9-231253
出願日： 1996年02月26日
公開日（公表日）： 1997年09月05日
要約：

【要約】【課題】指定された状態に到達させる際に、望ましくない状態や状態遷移を避けた検証データを生成して検証効率を向上させる。【解決手段】入力過程で、同期式順序回路の有限状態機械M、目標状態集合QT 及び障害状態集合QB が与えられると、像計算過程で、有限状態機械Mの初期状態集合Q0 から障害状態集合QB に含まれない次の状態集合を求める演算及び目標状態集合QT との共通集合を求める演算を繰り返し適用して、有限状態機械Mの初期状態集合Q0 から障害状態集合QB を通らずに到達可能な目標状態集合Q〜を求め、逆像計算過程で、到達可能な目標状態集合Q〜の中の任意の目標状態q〜から前の状態集合を求める演算を繰り返し適用して目標状態q〜から初期状態q0 に至る遷移列を求め、最後に入力系列抽出過程で、初期状態q0 から障害集合QB を通らずに目標状態q〜に到達させる入力系列を抽出する。

請求項（抜粋）：

同期式順序回路の動作を表す有限状態機械M、及び有限状態機械Mの状態集合Qに対する目標状態集合QT と障害状態集合QB を与える入力過程と、有限状態機械Mの初期状態集合Q0 から障害状態集合QB に含まれない次の状態集合を求める演算および目標状態集合QT との共通集合を求める演算を繰り返し適用して、有限状態機械Mの初期状態集合Q0 から障害状態集合QB を通らずに到達可能な目標状態集合Q〜を求める像計算過程と、前記像計算過程で求めた目標状態集合Q〜の中の任意の目標状態q〜から前の状態集合を求める演算を初期状態q0 に至るまで繰り返し適用することによって、目標状態q〜から初期状態集合Q0 に至る遷移列を求める逆像計算過程と、前記逆像計算過程で求めた遷移列から、初期状態q0 から障害状態集合QB を通らずに目標状態q〜に到達させる入力系列を抽出する入力系列抽出過程と、を備え、目標状態集合QT の中で障害状態集合QB を通らずに到達可能な目標状態集合Q〜の中のいずれかの目標状態q〜に到達させる入力系列を求めることを特徴とする有限状態機械の検証データ生成方法。

IPC (3件)：

G06F 17/50 ,  G01R 31/28 ,  G06F 11/25

FI (4件)：

G06F 15/60 664 B ,  G01R 31/28 F ,  G06F 11/26 310 ,  G06F 15/60 670