| 講演名 | 1994/11/17 論理ペトリネットを用いた形式仕様の自動変換と検証(グラフ,ネットワークとアルゴリズムおよび一般) 宋 国煥, 富樫 敦, 白鳥 則郎, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 通信システムの機能の高度化や大規模化に伴い,システムの要求が多様化・複雑化し,さらに要求の変更が頻発になってきている.以上の理由により,システムの仕様を形式化するのがますます困難になってきている.本論文では,システムに対する要求から得られた機能要求を,拡張ペトリネットの一種である論理ペトリネットを用いてモデル化し,論理的エラーを含んでいる機能要求を検証しながら,システムの形式仕様を自動的に生成する方法を提案する.本論文では,通信システムにおける形式記述技法の基本概念になっている状態遷移システムを形式仕様とする.本合成法は,システムの形式仕様を合成する際,実際必要な状態だけを生成する方法となっている. |
| 抄録(英) | In this paper, we propose a model, Logical Petri net (LPN), that is a kind of extended Petri net, in order to model functional requirements which come from system requirements. And we also propose a synthesis method that converts functional requirements of a system into formal specifications automatically, while searching functional requirements that contain some kinds of logical errors. We use the state transition systems as the formal specification descriptions, because it is the basic concept of the Formal Description Techniques (FDTs) for communication systems. When we create the state transition systems, the synthesis method produces states that are only necessary ones in the system. |
| キーワード(和) | ペトリネット / 可達木 / 形式仕様 / 検証 |
| キーワード(英) | Petri net / reachability tree / formal specification / verification |
| 資料番号 | CAS94-69,CST94-29 |
| 発行日 |
| 研究会情報 | |
| 研究会 | CST |
|---|---|
| 開催期間 | 1994/11/17(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Concurrent System Technology (CST) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 論理ペトリネットを用いた形式仕様の自動変換と検証(グラフ,ネットワークとアルゴリズムおよび一般) |
| サブタイトル（和） | |
| タイトル（英） | An Automatic Generation of Formal Specifications and Its Verification Using Logical Petri net |
| サブタイトル（和） | |
| キーワード(1)（和/英） | ペトリネット / Petri net |
| キーワード(2)（和/英） | 可達木 / reachability tree |
| キーワード(3)（和/英） | 形式仕様 / formal specification |
| キーワード(4)（和/英） | 検証 / verification |
| 第 1 著者 氏名（和/英） | 宋 国煥 / Kukhwan SONG |
| 第 1 著者 所属（和/英） | 東北大学電気通信研究所 Research Institute of Electrical Communication, Tohoku University |
| 第 2 著者 氏名（和/英） | 富樫 敦 / Atsushi TOGASHI |
| 第 2 著者 所属（和/英） | 東北大学電気通信研究所 Research Institute of Electrical Communication, Tohoku University |
| 第 3 著者 氏名（和/英） | 白鳥 則郎 / Norio SHIRATORI |
| 第 3 著者 所属（和/英） | 東北大学電気通信研究所 Research Institute of Electrical Communication, Tohoku University |
| 発表年月日 | 1994/11/17 |
| 資料番号 | CAS94-69,CST94-29 |
| 巻番号（vol） | vol.94 |
| 号番号（no） | 333 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |