遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証

情報処理学会 HANDLE Web Site 参考文献9件 オープンアクセス

書誌事項

タイトル別名
  • センイ　ノ　センタク　ガ　ジョウタイ　ホウモン　カイスウ　デ　キマル　ユウゲン　ジョウタイ　キカイ　ツイ　カラ　ナル　ツウシンケイ　二　タイスル　セイゾンセイ　ノ　ケンショウ
  • センイ ノ センタク ガ ジョウタイ ホウモン カイスウ デ キマル ユウゲン
  • Verification of Liveness Property for C - FSM's with Transitions depending on State Visiting Numbers
  • 通信技術

この論文をさがす

抄録

本論文では，各状態からの遷移条件がその状態の訪問回数で決まる有限状態機械モデルの上で生存性の検証を機械的に行う1つの方法を提案する．通信プロトコルは有限状態機械（FSM）によってモデル化され検証される場合が多いが，一般にシーケンス番号などのパラメータ値の変化を直接状態で区別して表そうとするとFSMの状態数が多くなり，状態爆発が起こる．我々は各遷移の実行可能性がその遷移の開始状態の訪問回数で決まるような有限状態機械モデルFSM／Cを提案し，このFSM／Cモデルの上で整数線形計画法を用いることにより状態爆発を回避した生存性の検証法を提案する．FSM／Cモデルでいくつかの通信プロトコルの仕様を記述できる．また，この手法に基づき，FSM／Cからなる通信系の生存性を検証するシステムを作成した結果についても報告する．

Many communication protocols are modeled as finite state machines(FSM's).In general,since the size of states becomes large in order to treat parameter values such as sequence numbers,the state explosion problem may occur.In this paper,we will propose an FSM/C model where the execution of each transition may depend on the number that its starting state has been visited,and propose a technique for verifying a liveness property.In this model,a counter Csi holds the number that state si has been visited.Many communication protocols can be modeled in our FSM/C model.If two communicating FSM/C's eventually return to the pair of their initial states and the communication channels become empty,thenwe say that they have the liveness property.For verifying the liveness property,we use an integer linear programming technique so that the state explosion problem does not occur.

収録刊行物

参考文献 (9)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ