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

• Item type: Journal(1)
• 公開日: 1998-03-15
• タイトル: 遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
• タイトル / 言語: en
• タイトル: Verification of Liveness Property for C - FSM's with Transitions depending on State Visiting Numbers
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• その他タイトル / その他のタイトル: 通信技術
• 著者所属: 大阪大学基礎工学部情報科学科
• 著者所属: 広島市立大学情報科学部情報数理学科
• 著者所属: 大阪大学基礎工学部情報科学科
• 著者所属: 大阪大学基礎工学部情報科学科
• 著者所属: 大阪大学基礎工学部情報科学科
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Faculty of Information Sciences, Hiroshima City University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, School of Engineering Science, Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences, School of Engineering Science, Osaka University
• 著者名: 水野, 健太郎; 中田, 明夫; 岡野, 浩三; 東野, 輝夫; 谷口, 健一
• 著者名(英): Kentaro, Mizuno; Akio, Nakata; Kozo, Okano; Teruo, Higashino; Kenichi, Taniguchi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，各状態からの遷移条件がその状態の訪問回数で決まる有限状態機械モデルの上で生存性の検証を機械的に行う1つの方法を提案する．通信プロトコルは有限状態機械（FSM）によってモデル化され検証される場合が多いが，一般にシーケンス番号などのパラメータ値の変化を直接状態で区別して表そうとするとFSMの状態数が多くなり，状態爆発が起こる．我々は各遷移の実行可能性がその遷移の開始状態の訪問回数で決まるような有限状態機械モデルFSM／Cを提案し，このFSM／Cモデルの上で整数線形計画法を用いることにより状態爆発を回避した生存性の検証法を提案する．FSM／Cモデルでいくつかの通信プロトコルの仕様を記述できる．また，この手法に基づき，FSM／Cからなる通信系の生存性を検証するシステムを作成した結果についても報告する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 39, 号 3, p. 750-759, 発行日 1998-03-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764