| No | 68126 |
|---|---|
| 標題（和） | 縮退到達可能性解析における網羅性について |
| 標題（英） | On Exhaustiveness of Reduced Reachability Analysis |
| 研究会名（和） | 交換システム; 情報ネットワ-ク; 通信方式 |
| 研究会名（英） | Switching Systems Engineering; Information Networks; Communieation Systems |
| 開催年月日 | 1995-09-28 |
| 終了年月日 | 1995-09-29 |
| 会議種別コード | 2 |
| 共催団体名（和） | |
| 資料番号 | SSE95-68 // IN95-39 // CS95-88 |
| 抄録（和） | 本稿ではロ-カルなル-プを含む通信有限状態遷移仕様に対する縮退到達可能性解析の網羅性について議論する。通信有限状態遷移仕様からメッセ-ジシ-ケンスチャ-トを抽出するとき、洩れなく抽出されているかという網羅性が問題となる。縮退到達可能解析を用いて抽出を行なう場合の網羅性を示すには、一般の到達可能性解析で得られる全ての動作系列に対し、対応する動作系列が縮退到達可能性解析により得られることを示せばよい。本稿ではこの証明を与え、縮退到達可能性解析を用いたメッセ-ジシ-ケンスチャ-トの抽出が網羅性を保証することが可能であることを示す。 |
| 抄録（英） | 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 Analvsis with an execution trace obtained by a general Reachability Analysis.It means we can retrieve MSCs from a CFSM specification exhaustively. |
| 収録資料名（和） | 電子情報通信学会技術研究報告 |
| 収録資料の巻号 | Vol.95 No.266〜271 |
| ページ開始 | 88 |
| ページ終了 | 90 |
| キーワード（和） | 仕様記述 |
| キーワード（英） | Specification |
| 本文の言語 | JPN |
| 著者（和） | 平川豊 |
| 著者（ヨミ） | ヒラカワユタカ |
| 著者（英） | Hirakawa Yutaka |
| 所属機関（和） | NTTソフトウェア研究所 |
| 所属機関（英） | NTT Software Laboratories |
| 著者（和） | 荒川則泰 |
| 著者（ヨミ） | アラカワノリヤス |
| 著者（英） | Arakawa Noriyasu |
| 所属機関（和） | NTTソフトウェア研究所 |
| 所属機関（英） | NTT Software Laboratories |
| 著者（和） | 大友健治 |
| 著者（ヨミ） | オオトモケンジ |
| 著者（英） | Otomo Kenji |
| 所属機関（和） | NTTソフトウェア研究所 |
| 所属機関（英） | NTT Software Laboratories |