特許

J-GLOBAL ID：200903026852495035

静的半順序換算

発明者： ロバート ポール カーシャン ,  ヴラッドミール レヴィン ,  マリウス ミネア ,  ドロン エー. ペレド ,  ハスヌ エニガン
出願人/特許権者： ルーセント テクノロジーズ インコーポレーテッド
代理人 (1件)： 岡部 正夫 (外11名)
公報種別：公開公報
出願番号（国際出願番号）：特願平10-313128
公開番号（公開出願番号）：特開2000-207428
出願日： 1998年11月04日
公開日（公表日）： 2000年07月28日
要約：

【要約】【課題】 本発明は、システム仕様換算法に関する。【解決手段】 静的半順序換算ゼネレータと処理は、モデル検査処理と無関係に、多重処理システムの大きく換算された状態空間グラフに帰結する。本発明の処理は、状態と遷移が検証の過程で検討される場合、どんな望ましい状態探索戦術(幅優先、深さ優先等)も利用できるようにする規則の追加された修正された状態グラフ・ゼネレータを作成する。これによって、既存のモデル検査ツールを修正なしに使用することが可能になる。静的半順序換算は、換算された状態グラフの各サイクルに沿った少なくとも1つの状態が完全に展開されなければならないという従来技術の条件が、システムを構成する個々の処理を検討し、それらの処理中のある遷移を特定することによって保証されるということを実現することによって可能になる。

請求項（抜粋）：

多重処理システムを記述する所定の状態グラフ・ゼネレータと、前記増補状態グラフ・ゼネレータを形成する所定の状態を増補する規則の集合とを含む増補状態グラフ・ゼネレータであって、該改善が、規則の前記集合に含まれる、状態グラフの静的作成を可能にする規則を含む増補ゼネレータ。

FI (4件)：

G06F 15/60 664 J ,  G06F 15/60 636 G ,  G06F 15/60 654 A ,  G06F 15/60 664 A

Fターム (4件)：

5B046AA08 ,  5B046BA01 ,  5B046DA04 ,  5B046JA01

引用特許：

審査官引用 (3件)

• 順序回路の到達可能状態計算装置
  公報種別：公開公報   出願番号：特願平10-060982   出願人：富士通株式会社
• プロパティ検証方法および装置
  公報種別：公開公報   出願番号：特願平8-220005   出願人：富士通株式会社
• 特開平4-219804