| 講演名 | 1994/1/14 プロダクションシステムを用いた通信ソフトウェア仕様の可到達解析に関する考察 佐藤 正和, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 通信ソフトウェア仕様の重要な検証項目の一つとして,状態の可到達性解析,即ち,特定の状態が,ある仕様によって与えられたシステムに出現するか否かの検査がある.本稿では,書き換え型のプロダクションシステムによって定義された通信ソフトウェア仕様の可到達集合についてその基本的な性質を考察する.可到達状態を複数のプロセスによって構成される到達可能な準広域状態として定義したとき,可到達状態集合の大きさは,初期状態として与えるプロセス数を増やすと単調増加することが予想される.このため可到達性を一般に保証するには,プロセス数を無限と仮定した解析を行なう必要がある.本論文では,システムを構成するプロセス数と可到達集合の大きさの関係を明らかにし,最大の可到達集合を得るのに必要な最小のプロセス数を求める方法を示した.これによって,無限プロセスの存在を仮定するシステムの可到達性を有限プロセスのそれに置き替えて議論することが可能になった. |
| 抄録(英) | Reachability analysis,which decides a specific state appearance in a specified system,is a major task of specification verification of communication systems.In this paper,the characteristics of a rearchable set of communication software specifications,defined using re-writable type production system,is discussed.Assuming to define reachable states as reachable semi- global states including multiple processes,the size of a reachable set is predicted to be monotone increasing about the number of processes in the system.Therefore,in order to guarantee reachability in general cases,the system including infinite number of processes should be assumed.In this paper,the functional relation between the number of processes and reachable sets is clarified,and an algorithm to obtain a minimum number of processes giving the largest set of reachable states.Consideration of this number of processes makes it possible to analyze this kind of system. |
| キーワード(和) | 仕様記述 / 仕様検証 / プログラム検証 / 可到達解析 / プロダクションシステム |
| キーワード(英) | Specification description / Specification verification / Program verification / Reachability analysis |
| 資料番号 | KBSE93-45 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 1994/1/14(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | プロダクションシステムを用いた通信ソフトウェア仕様の可到達解析に関する考察 |
| サブタイトル（和） | |
| タイトル（英） | A Reachability Analysis for Communication Software Specifications by Production System |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 仕様記述 / Specification description |
| キーワード(2)（和/英） | 仕様検証 / Specification verification |
| キーワード(3)（和/英） | プログラム検証 / Program verification |
| キーワード(4)（和/英） | 可到達解析 / Reachability analysis |
| キーワード(5)（和/英） | プロダクションシステム |
| 第 1 著者 氏名（和/英） | 佐藤 正和 / Masakazu Sato |
| 第 1 著者 所属（和/英） | ATR通信システム研究所 Communication Systems Research Laboratories,ATR |
| 発表年月日 | 1994/1/14 |
| 資料番号 | KBSE93-45 |
| 巻番号（vol） | vol.93 |
| 号番号（no） | 408 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |