外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法  [in Japanese] Symbolic Model Checking of Extended Finite State Machines with Linear Constraints over Integer Variables  [in Japanese]

Access this Article

Search this Article

Author(s)

Abstract

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

Journal

  • The Transactions of the Institute of Electronics,Information and Communication Engineers.

    The Transactions of the Institute of Electronics,Information and Communication Engineers. 87(4), 462-470, 2004-04-01

    The Institute of Electronics, Information and Communication Engineers

References:  10

Codes

  • NII Article ID (NAID)
    110003171323
  • NII NACSIS-CAT ID (NCID)
    AA11341020
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09151915
  • NDL Article ID
    6913287
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-779
  • Data Source
    CJP  NDL  NII-ELS  IR 
Page Top