| 講演名 | 1995/9/28 縮退到達可能性解析における網羅性について 大友 健治, 荒川 則泰, 平川 豊, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿ではローカルなループを含む通信有限状態遷移仕様に対する縮退到達可能性解析の網羅性について議論する。通信有限状態遷移仕様からメッセージシーケンスチャートを抽出するとき、洩れなく抽出されているかという網羅性が問題となる。縮退到達可能性解析を用いて抽出を行なう場合の網羅性を示すには、一般の到達可能性解析で得られる全ての動作系列に対し、対応する動作系列が縮退到達可能性解析により得られることを示せばよい。本稿ではこの証明を与え、縮退到達可能性解析を用いたメッセージシーケンスチャートの抽出が網羅性を保証することが可能であることを示す。 |
| 抄録(英) | In this paper, we discuss the exhaustiveness of Reduced Reachability Analysis when it analyze a Communication Finite State Machine (CFSM) specification which contains local loops. When we retrieve Message Sequence Charts (MSCs) from a CFSM specification, it is important that there should be no deficiency in the MSCs. We prove that there exists a corresponding execution trace obtained by Reduced Reachability Analysis with an execution trace obtained by a general Reachability Analysis. It means we can retrieve MSCs from a CFSM specification exhaustively. |
| キーワード(和) | 通信ソフトウェア / メッセージシーケンスチャート / 網羅性 / 到達可能性解析 / 仕様記述 |
| キーワード(英) | Communications Software / Message Sequence Chart / Exhaustiveness / Reachability Analysis / Specification |
| 資料番号 | SSE95-68,IN95-39,CS95-88 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SSE |
|---|---|
| 開催期間 | 1995/9/28(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Switching Systems Engineering (SSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 縮退到達可能性解析における網羅性について |
| サブタイトル（和） | |
| タイトル（英） | On Exhaustiveness of Reduced Reachability Analysis |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 通信ソフトウェア / Communications Software |
| キーワード(2)（和/英） | メッセージシーケンスチャート / Message Sequence Chart |
| キーワード(3)（和/英） | 網羅性 / Exhaustiveness |
| キーワード(4)（和/英） | 到達可能性解析 / Reachability Analysis |
| キーワード(5)（和/英） | 仕様記述 / Specification |
| 第 1 著者 氏名（和/英） | 大友 健治 / Kenji Otomo |
| 第 1 著者 所属（和/英） | NTTソフトウェア研究所 NTT Software Laboratories |
| 第 2 著者 氏名（和/英） | 荒川 則泰 / Noriyasu Arakawa |
| 第 2 著者 所属（和/英） | NTTソフトウェア研究所 NTT Software Laboratories |
| 第 3 著者 氏名（和/英） | 平川 豊 / Yutaka Hirakawa |
| 第 3 著者 所属（和/英） | NTTソフトウェア研究所 NTT Software Laboratories |
| 発表年月日 | 1995/9/28 |
| 資料番号 | SSE95-68,IN95-39,CS95-88 |
| 巻番号（vol） | vol.95 |
| 号番号（no） | 266 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |