外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法

竹中, 崇; 岡野, 浩三; 東野, 輝夫 他

電子情報通信学会論文誌D, 2004, J87-D1(4), 462-470

アクセス数:277件（2025-03-19 18:51 集計）

固定URL: https://hdl.handle.net/11094/27431

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
IEICE_J87-D1_4_462 pdf なし 341 KB 250 2014.04.11  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法
Symbolic Model Checking of Extended Finite State Machines with Linear Constraints over Integer Variables
ガイブ　ニュウリョクチ　ノミ　ヲ　ホジ　デキル　セイスウ　ヘンスウ　ヲ　モツ　FSM　ニ　タイスル　キゴウ　モデル　ケンサホウ
著者
著者名
竹中, 崇 ; タケナカ, タカシ ; Takenaka, Takashi
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000080173144 1000080173144
researchmap permalink
teruo.higashino teruo.higashino
Scopus Author ID
7005648670 7005648670
著者名
東野, 輝夫 ; ヒガシノ, テルオ ; Higashino, Teruo
NRID
1000000029513 1000000029513
著者名
谷口, 健一 ; タニグチ, ケンイチ ; Taniguchi, Kenichi
キーワード等
記号モデル検査
CTL
プレスブルガー文
抄録
整数変数をもつ有限状態機械（FSM/int）に対する記号モデル検査法を提案する．入力値を保持する変数の値は次に同一遷移で新たな値が読み込まれるまで変更されない，などの制約を満たす，与えられたFSM/intに対し，整数変数をもつCTL式を満たすか否かをこの記号検査アルゴリズムは判定する．この記号モデル検査アルゴリズムを実装し，ブラックジャックディーラ回路とパケット多重化プロトコルに適用した．そして，100状態，10整数変数程度の規模のシステムであれば数秒程度（最悪時で数分程度）で検証できることが確かめられた．
出版者
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名
電子情報通信学会論文誌D
巻(号)
J87-D1(4)
ページ
462-470
刊行年月
2004-04-01
言語
日本語
ハンドルURL
https://hdl.handle.net/11094/27431
PISSN
09151915
NCID
AA11341020
関連情報 (references)
URI
http://search.ieice.org/
アクセス権
open access
権利情報
Copyright © 2004 IEICE
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article