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

• 竹中, 崇

• 岡野, 浩三

• 東野, 輝夫

• 谷口, 健一

書誌事項

タイトル別名

• Symbolic Model Checking of Extended Finite State Machines with Linear Constraints over Integer Variables
• ガイブ　ニュウリョクチ　ノミ　ヲ　ホジ　デキル　セイスウ　ヘンスウ　ヲ　モツ　FSM　ニ　タイスル　キゴウ　モデル　ケンサホウ

抄録

整数変数をもつ有限状態機械（FSM/int）に対する記号モデル検査法を提案する．入力値を保持する変数の値は次に同一遷移で新たな値が読み込まれるまで変更されない，などの制約を満たす，与えられたFSM/intに対し，整数変数をもつCTL式を満たすか否かをこの記号検査アルゴリズムは判定する．この記号モデル検査アルゴリズムを実装し，ブラックジャックディーラ回路とパケット多重化プロトコルに適用した．そして，100状態，10整数変数程度の規模のシステムであれば数秒程度（最悪時で数分程度）で検証できることが確かめられた．

収録刊行物

• 電子情報通信学会論文誌D

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

  電子情報通信学会

キーワード

• 記号モデル検査
• CTL
• プレスブルガー文

詳細情報

• CRID: 1050862643881187200
• NII論文ID: 110003171323
• NII書誌ID: AA11341020
• HANDLE: 11094/27431
• NDL書誌ID: 6913287
• ISSN: 09151915
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I6913287
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles