| 講演名 | 2011-11-18 上流設計からモデル検査プロセスまでの一貫設計検証環境 : UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法(提案型エンタプライズモデリング ワークショップ) 宮本 直樹, 和崎 克己, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | SPINモデル検査器を実行するには,専用の仕様記述言語PROMELAで対象モデルを記述する.また,検査対象の仕様の記述には線形時相論理(LTL)式を用いる.本研究では,システム開発の上流設計段階で使われるUML図を,PROMELAコード及びLTL式に自動変換する手法を提案する.UMLのステートマシン図と配置図を組みで利用し,ステートマシン図に,対象モデルの振る舞いや配置状況,要求仕様を記述し,PROMELAコードへの自動変換を実現する.一方,要求仕様として,UMLのシーケンス図を仕様パターンに準拠した記法に制限・展開することで,LTL式の自動生成を実現する.以上の機能を有する援用ツール群を試作し,ある通信プロトコルを対象とした上位設計に対する自動変換を実施し,評価を行った. |
| 抄録(英) | 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. |
| キーワード(和) | 上流設計 / モデル検査 / UML / SPIN / PROMELA / 線形時相論理式 / 仕様パターン |
| キーワード(英) | Upstream Design / Model Checking / UML / SPIN / PROMELA / Linear Temporal Logic / Specification Patterns |
| 資料番号 | SWIM2011-19 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SWIM |
|---|---|
| 開催期間 | 2011/11/11(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Interprise Modeling (SWIM) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 上流設計からモデル検査プロセスまでの一貫設計検証環境 : UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法(提案型エンタプライズモデリング ワークショップ) |
| サブタイトル（和） | |
| タイトル（英） | 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 |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 上流設計 / Upstream Design |
| キーワード(2)（和/英） | モデル検査 / Model Checking |
| キーワード(3)（和/英） | UML / UML |
| キーワード(4)（和/英） | SPIN / SPIN |
| キーワード(5)（和/英） | PROMELA / PROMELA |
| キーワード(6)（和/英） | 線形時相論理式 / Linear Temporal Logic |
| キーワード(7)（和/英） | 仕様パターン / Specification Patterns |
| 第 1 著者 氏名（和/英） | 宮本 直樹 / Naoki MIYAMOTO |
| 第 1 著者 所属（和/英） | 信州大学大学院工学系研究科 Faculty of Engineering, Graduate School of Science and Technology, Shinshu University |
| 第 2 著者 氏名（和/英） | 和崎 克己 / Katsumi WASAKI |
| 第 2 著者 所属（和/英） | 信州大学工学部情報工学科 Faculty of Engineering, Shinshu University |
| 発表年月日 | 2011-11-18 |
| 資料番号 | SWIM2011-19 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | 308 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |