| Presentation | 2000/11/10 Formalization and Verification of the Enterprise JavaBeans~TM Server Specification Shin NAKAJIMA, Tetsuo TAMAI, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Component / Formal Methods / Behavioural Specifications / Model-Checking |
| Paper # | KBSE2000-47 |
| Date of Issue |
| Conference Information | |
| Committee | KBSE |
|---|---|
| Conference Date | 2000/11/10(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Formalization and Verification of the Enterprise JavaBeans~TM Server Specification |
| Sub Title (in English) | |
| Keyword(1) | Component |
| Keyword(2) | Formal Methods |
| Keyword(3) | Behavioural Specifications |
| Keyword(4) | Model-Checking |
| 1st Author's Name | Shin NAKAJIMA |
| 1st Author's Affiliation | C&C Media Research Laboratories NEC Corporation() |
| 2nd Author's Name | Tetsuo TAMAI |
| 2nd Author's Affiliation | Interfaculty Initiative in Information Studies Graduate School of The University of Tokyo |
| Date | 2000/11/10 |
| Paper # | KBSE2000-47 |
| Volume (vol) | vol.100 |
| Number (no) | 441 |
| Page | pp.pp.- |
| #Pages | 8 |
| Date of Issue | |