| 講演名 | 1999/1/23 振舞仕様に基づくAddress Resolution Protocolの仕様記述 海野 浩, 二木 厚吉, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 振舞仕様は, システムがどのように実装されるかではなく, システムがどのように外部観測的に振舞うかを規定する.振舞等価性は, 観測を通して等しいとされる二つの状態は区別がつかないという概念に基づいている.代数仕様言語CafeOBJはこの振舞仕様をサポートする.射影演算は振舞仕様の合成において重要な役割を果たし, 証明の再利用を可能にする.本稿では, 振舞仕様に基づく仕様記述法を, データ転送を伴う単純な同期通信システムと, Address Resolution Protocolと呼ばれる通信処理システムに適用し, この方法の有効性を検討する. |
| 抄録(英) | Behavioural specification characterize how systems behave, not how they are implemented.Behavioural equivalence is besed on the idea of indistinguishability of states that are observationally the same.Algebraic specification language CafeOBJ supports behavioural specification. Projection operator plays an important role when we will compose behavioural specifications, and it supports reusability of proofs.In this paper, we study the method to specify concurrent systems, a simple communication system with data transfer, and The Address Resolution Protocol, by using behavioural specification. |
| キーワード(和) | 形式手法 / 形式仕様 / 代数仕様 / 振舞仕様 / 隠蔽代数 / 並行システム |
| キーワード(英) | Formal Methods / formal specification / Algebraic specification / behavioural specification / hidden algebra / concurrent systems |
| 資料番号 | SS98-49 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1999/1/23(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 振舞仕様に基づくAddress Resolution Protocolの仕様記述 |
| サブタイトル（和） | |
| タイトル（英） | Specifying The Address Resolution Protocol by using Behavioural Specifications |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式手法 / Formal Methods |
| キーワード(2)（和/英） | 形式仕様 / formal specification |
| キーワード(3)（和/英） | 代数仕様 / Algebraic specification |
| キーワード(4)（和/英） | 振舞仕様 / behavioural specification |
| キーワード(5)（和/英） | 隠蔽代数 / hidden algebra |
| キーワード(6)（和/英） | 並行システム / concurrent systems |
| 第 1 著者 氏名（和/英） | 海野 浩 / Hiroshi Unno |
| 第 1 著者 所属（和/英） | 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Japan Advanced Institute of Science and Technology |
| 第 2 著者 氏名（和/英） | 二木 厚吉 / Kokichi Futatsugi |
| 第 2 著者 所属（和/英） | 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Japan Advanced Institute of Science and Technology |
| 発表年月日 | 1999/1/23 |
| 資料番号 | SS98-49 |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 559 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |