| 講演名 | 2000/11/10 Enterprise JavaBeans~TMサーバ仕様の形式化と検証 中島 震, 玉井 哲雄, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 分散コンポーネット基盤フレームワークでは構成コンポーネント間でのイベント系列(振舞い仕様)が重要な側面であり、厳密に規定されている必要がある。本稿では実用的な分散コンポーネント基盤であるEnterprise JavaBeans~TM(EJB)サーバ仕様を形式化し、モデル検査ツールSPINを用いて解析を行なうことで、EJB仕様書の正しさを振舞い仕様の観点から確認する。SPINによる形式化と検証によって、仕様書が明記していない暗黙の状態管理が必要であること、等が判明した。また、本具体例を通して、SPINが分散アーキテクチャ検証のためのデザイン言語として良い特徴を持つこと、ならびに試行錯誤的な検証過程を容易にする「軽い(Lightweight)」デザインカリキュレータとして有用であること、等がわかった。 |
| 抄録(英) | Rigorous description of protocols(a sequence of events)between components is mandatory for specifications of distributed component server frameworks.This paper reports an experience in formalizing and verifying behavioural aspects of the Enterprise JavaBeans~TM server specification with the SPIN model-checker.The formal model helps uncover server states necessary for a proper management of components.The present case study shows that SPIN has useful features for analyzing behaviour of distributed software architecture, and that SPIN can be used as a lightweight design calculator in the verification process. |
| キーワード(和) | コンポーネント / 形式手法 / 振舞い仕様 / モデルチェッキング |
| キーワード(英) | Component / Formal Methods / Behavioural Specifications / Model-Checking |
| 資料番号 | KBSE2000-47 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2000/11/10(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | Enterprise JavaBeans~TMサーバ仕様の形式化と検証 |
| サブタイトル（和） | |
| タイトル（英） | Formalization and Verification of the Enterprise JavaBeans~TM Server Specification |
| サブタイトル（和） | |
| キーワード(1)（和/英） | コンポーネント / Component |
| キーワード(2)（和/英） | 形式手法 / Formal Methods |
| キーワード(3)（和/英） | 振舞い仕様 / Behavioural Specifications |
| キーワード(4)（和/英） | モデルチェッキング / Model-Checking |
| 第 1 著者 氏名（和/英） | 中島 震 / Shin NAKAJIMA |
| 第 1 著者 所属（和/英） | NEC情報通信メディア研究本部 C&C Media Research Laboratories NEC Corporation |
| 第 2 著者 氏名（和/英） | 玉井 哲雄 / Tetsuo TAMAI |
| 第 2 著者 所属（和/英） | 東京大学大学院情報学環 Interfaculty Initiative in Information Studies Graduate School of The University of Tokyo |
| 発表年月日 | 2000/11/10 |
| 資料番号 | KBSE2000-47 |
| 巻番号（vol） | vol.100 |
| 号番号（no） | 441 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |