ECFSMモデル通信プロトコルの検証システムにおける不変式の自動生成

• Item type: SIG Technical Reports(1)
• 公開日: 1995-05-25
• タイトル: ECFSMモデル通信プロトコルの検証システムにおける不変式の自動生成
• タイトル / 言語: en
• タイトル: Automatic Generation of Invariant Formula for Communication Protocols Modeled as ECFSMs
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属: 大阪大学基礎工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences Osaka University
• 著者所属(英): en
• 著者所属(英): Department of Information and Computer Sciences Osaka University
• 著者名: 樋口, 昌宏; 玉井, 順子; 原, 圭吾; 藤井, 護
• 著者名(英): Masahiro, Higuchi; Junko, Tamai; Keigo, Hara; Mamoru, Fujii
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 筆者らは，プロトコル機械が拡張有限状態機械でモデル化され，通信路が非有界FIFOでモデル化された通信プロトコルの安全性，生存性の検証法を提案している．提案している検証法では，人間の検証者が記述した検証対象であるプロトコルに関する不変式を基に，検証システムがそのプロトコルの安全性，あるいは生存性を検証する．この検証法では，不変式の記述に要する検証者の作業量が大きなものとなってしまうという問題点がある．本稿では，不変式記述作業の軽減を目的に，積和形で記述される不変式の積項のうち，一方のプロトコル機械のメッセージの送信に同期して他方のプロトコル機械のメッセージの受信が行なわれる同期型通信で到達可能な状態と，それらの状態からメッセージの送信のみによって到達可能な状態で成り立つ積項を自動生成する手法を提案する．提案する手法に基づく積項の自動生成システムを試作し，OSIセションプロトコルのデータ転送フェーズから抽出した例プロトコルに適用したところ，不変式の積項472個のうち445個の積項を自動生成することができた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Previously, we proposed a verification method via invariant for communication protocols modeled as ECFSMs. In the proposed method, a human verifier describes an invariant of a given protocol, and a verification system shows safety or liveness using the invariant. The tedious work on describing invariant formula is a significant shortcoming of the proposed method. This paper deal with a semiautomated derivation of invariant formula for communication protocols modeled as ECFSMs. In the method, formula holds on the states, which is reachable by synchronous communication and sending transitions, are automatically derived. We conducted an experiment on deriving disjuncts of invariant formula of a sample protocol extracted from the OSI session protocol. Among 472 disjuncts of an invariant formula, 445 disjuncts are automatically derived.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10116224
• 書誌情報: 情報処理学会研究報告マルチメディア通信と分散処理（DPS）; 巻 1995, 号 53(1995-DPS-070), p. 105-110, 発行日 1995-05-25
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会