特許
J-GLOBAL ID：200903089708943190
形式的検証方法
発明者：
出願人/特許権者：
代理人 (1件)：
▲柳▼川 信
公報種別：公開公報
出願番号（国際出願番号）：特願平11-205509
公開番号（公開出願番号）：特開2001-034641
出願日： 1999年07月21日
公開日（公表日）： 2001年02月09日
要約：
【要約】【課題】 異常状態からの自己復旧の可否を検証可能な形式的検証方法を提供する。【解決手段】 ステップS1で回路記述入力されると、ステップS2で回路記述の構文解析が行われた後、ステップS3でKripke構造の有限状態機械に変換される。ステップS4で初期状態集合Voから到達できる節点の集合を全体集合Vの中から求め、正常節点の集合Vnとし、ステップS5で全体集合Vの中で正常節点の集合Vnに属さない節点の集合を求め、異常節点の集合Vxとする。ステップS6で異常節点の集合Vxに属する全ての節点から、正常節点の集合Vnに属するどれかの節点へ到達できるかどうかを検索する。ステップS7で検索結果が真と判定されると、ステップS8で異常状態から復帰可能と通知し、検索結果が偽と判定されると、ステップS9で異常状態から復帰不可と通知する。
請求項（抜粋）：
動作記述及び回路接続情報の一方で表される同期式順序回路の動作を表す有限状態機械において検証仕様を満足しているかどうかを検証する形式的検証方法であって、起こり得ない状態を示す異常状態を有限状態の一部として表現し、前記異常状態をも含めた状態遷移を考慮するようにしたことを特徴とする形式的検証方法。
Fターム (4件)：
5B046AA08
, 5B046BA02
, 5B046DA06
, 5B046JA01
