- 著者
-
竹中 崇
岡野 浩三
東野 輝夫
谷口 健一
- 出版者
- 一般社団法人電子情報通信学会
- 雑誌
- 電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理 (ISSN:09151915)
- 巻号頁・発行日
- vol.87, no.4, pp.462-470, 2004-04-01
- 参考文献数
- 10
整数変数をもつ有限状態機械(FSM/int)に対する記号モデル検査法を提案する.入力値を保持する変数の値は次に同一遷移で新たな値が読み込まれるまで変更されない,などの制約を満たす,与えられたFSM/intに対し,整数変数をもつCTL式を満たすか否かをこの記号検査アルゴリズムは判定する.この記号モデル検査アルゴリズムを実装し,ブラックジャックディーラ回路とバケット多重化プロトコルに適用した.そして,100状態,10整数変数程度の規模のシステムであれば数秒程度(最悪時で数分程度)で検証できることが確かめられた.