Pat
J-GLOBAL ID：200903043217305655
プロセス制御論理の検証方法および装置
Inventor：
,
,
,
Applicant, Patent owner：
Agent (1)：
木内 光春
Gazette classification：公開公報
Application number (International application number)：1995255364
Publication number (International publication number)：1997097279
Application date： Oct. 02, 1995
Publication date： Apr. 08, 1997
Summary：
【要約】【課題】 制御論理が状態遷移図として記述された仕様を満たしていることを自動検証するプロセス制御論理の検証方法および装置を提供する。【解決手段】 プロセス制御論理から、その制御論理を論理式に置き換えることにより順序機械を抽出するステップ1。状態遷移図を論理式に置き換えることにより状態遷移機械を抽出するステップ2。それぞれの初期状態にある順序機械と状態遷移機械に任意の入力列を与えたときに順序機械と状態遷移機械のそれぞれが到達する状態について、その状態の対応を計算するステップ3。前記任意の入力列の入力によって到達した状態遷移機械の各状態のアクションについて、状態遷移機械の各状態に対応する順序機械の状態において、前記アクションと整合する出力が順序機械から出力されることを検査するステップ4。これらステップ1〜4によってプロセス制御論理と状態遷移図が整合していることを検証する。
Claim (excerpt)：
入力列とそれに対応する出力列を有するプロセス制御論理と、そのプロセス制御論理の仕様を、プロセス制御論理が取り得る各状態と各状態を結ぶ遷移、遷移条件および各状態におけるアクションにより表現した状態遷移図について、プロセス制御論理から、その制御論理を論理式に置き換えることにより順序機械を抽出するステップと、状態遷移図から、遷移条件およびアクションを論理式に置き換えることにより状態遷移機械を抽出するステップと、それぞれの初期状態にある順序機械と状態遷移機械に任意の入力列を与えたときに順序機械と状態遷移機械のそれぞれが到達する状態の対応を計算するステップと、前記任意の入力列の入力によって到達した状態遷移機械の各状態のアクションについて、状態遷移機械の各状態に対応する順序機械の状態において、状態遷移図のその状態から抜けないという条件の下での任意の入力列の入力に応じて、前記アクションと整合する出力が順序機械から出力されることを検査するステップとを含み、これら各ステップによってプロセス制御論理と状態遷移図とが整合していることを検証することを特徴とするプロセス制御論理の検証方法。
IPC (2)：
FI (2)：
G06F 15/60 664 G
, G05B 19/05 D
