| 講演名 | 2008-05-23 UNLシーケンス図におけるモデル検証方法(Web2.0時代のビジネスモデル) 高谷 彰俊, 新川 芳行, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本研究おいてモデル検査ツールSPINを使ったシーケンス図の検証方法を提案する。SPINはモデル記述をPromelaという状態遷移記述のための言語を用いて行うため、UMLシーケンス図を直接入力することはできない。このシーケンス図をPromelaに変換するため、SPINが想定する状態遷移モデルに近いUMLステートマシン図に一旦変換しここからPromelaコードを生成する手法を取った。生成されたPromelaコードの検証にはモデルに対する制約条件を表す時相論理式(LTL式)が必要となるがシーケンス図自体には制約条件が一般に含まれないため、最終状態への可達性を制約条件とする検査を行った。これにより、SPINによるシーケンス図の基本的な振る舞の検証が可能であることが確認できた。 |
| 抄録(英) | In this paper, we propose a verification process for UML sequence diagrams, using the SPIN model checker. The SPIN can not deal with UML sequence diagrams directly, since it can only deal with the models written in Promela, which describe state transitions. In order to transform the sequence diagrams into Promela codes, we first transform them into UML state-machine diagrams, which resemble the state-transition models that the SPIN assumes. The state-machine diagrams are then transformed into Promela codes. The temporal logic formulae (LTL formulae) are required as a constraint for the verification of the Promela codes, however no constraints are included in the original sequence diagrams. Therefore, the reachability to the final state is used as the constraint for the verification. As a result, the SPIN can verify the basic behavior of the sequence diagrams. |
| キーワード(和) | モデル検査 / UML / Promela / LTL |
| キーワード(英) | Model Verification / UML / Promela / LTL |
| 資料番号 | SWIM2008-3 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SWIM |
|---|---|
| 開催期間 | 2008/5/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Interprise Modeling (SWIM) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | UNLシーケンス図におけるモデル検証方法(Web2.0時代のビジネスモデル) |
| サブタイトル（和） | |
| タイトル（英） | Model Verification for UML Sequence Diagrams |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model Verification |
| キーワード(2)（和/英） | UML / UML |
| キーワード(3)（和/英） | Promela / Promela |
| キーワード(4)（和/英） | LTL / LTL |
| 第 1 著者 氏名（和/英） | 高谷 彰俊 / Akitoshi Takaya |
| 第 1 著者 所属（和/英） | 龍谷大学理工学研究科情報メディア学専攻 Graduate School of Science & Technology, Ryukoku University |
| 第 2 著者 氏名（和/英） | 新川 芳行 / Yoshiyuki Shinkawa |
| 第 2 著者 所属（和/英） | 龍谷大学理工学研究科情報メディア学専攻 Graduate School of Science & Technology, Ryukoku University |
| 発表年月日 | 2008-05-23 |
| 資料番号 | SWIM2008-3 |
| 巻番号（vol） | vol.108 |
| 号番号（no） | 56 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |