| Presentation | 2011-11-18 An Integrated Design and Verification Environment from Upstream Design to Model Checking Process : Automatic Conversion from UML Descriptions into the Process Definitions and Linear Temporal Logic for SPIN Model Checker Naoki MIYAMOTO, Katsumi WASAKI, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | To execute a SPIN model checker, the targeted model has to be described by the dedicated specification description language "PROMELA". Also, linear temporal logical (LTL) expressions are used for the description of the specification to be tested. In this study, we propose a method for automatically transforming the UML diagram used at the upstream design stage of system development to PROMELA codes and LTL expressions. Automatic transformation to PROMELA codes is achieved by the following procedures: (1) Combine the state machine chart and layout drawing of UML; and (2) Describe the behavior, layout condition, and requested specifications of the targeted model to the state machine chart. Meanwhile, as a requested specification, by restricting and expanding the sequence diagram of UML to a notation complying with the specification pattern, automatic generation of LTL expressions is achieved. We made computer-aided tools that have the functions above experimentally, and conducted evaluations of this method based on a case study of design verification. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Upstream Design / Model Checking / UML / SPIN / PROMELA / Linear Temporal Logic / Specification Patterns |
| Paper # | SWIM2011-19 |
| Date of Issue |
| Conference Information | |
| Committee | SWIM |
|---|---|
| Conference Date | 2011/11/11(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 | Software Interprise Modeling (SWIM) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | An Integrated Design and Verification Environment from Upstream Design to Model Checking Process : Automatic Conversion from UML Descriptions into the Process Definitions and Linear Temporal Logic for SPIN Model Checker |
| Sub Title (in English) | |
| Keyword(1) | Upstream Design |
| Keyword(2) | Model Checking |
| Keyword(3) | UML |
| Keyword(4) | SPIN |
| Keyword(5) | PROMELA |
| Keyword(6) | Linear Temporal Logic |
| Keyword(7) | Specification Patterns |
| 1st Author's Name | Naoki MIYAMOTO |
| 1st Author's Affiliation | Faculty of Engineering, Graduate School of Science and Technology, Shinshu University() |
| 2nd Author's Name | Katsumi WASAKI |
| 2nd Author's Affiliation | Faculty of Engineering, Shinshu University |
| Date | 2011-11-18 |
| Paper # | SWIM2011-19 |
| Volume (vol) | vol.111 |
| Number (no) | 308 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |