| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2011-11-18 10:30 上流設計からモデル検査プロセスまでの一貫設計検証環境 ～ UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法 ～ ○宮本直樹・和崎克己（信州大）  SWIM2011-19 |
|
| 抄録 | （和） | 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 specifi- cation 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 / PROMELA / 線形時相論理 / 仕様パターン / / |
| （英） | Upstream Design / Model Checking / UML / SPIN / PROMELA / Linear Temporal Logic / Specification Patterns / | |
| 文献情報 | 信学技報, vol. 111, no. 308, SWIM2011-19, pp. 7-12, 2011年11月. | |
| 資料番号 | SWIM2011-19 | |
| 発行日 | 2011-11-11 (SWIM) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SWIM2011-19 |
|
| 研究会情報 | |
| 研究会 | SWIM |
| 開催期間 | 2011-11-18 - 2011-11-18 |
| 開催地（和） | 東海大学 高輪キャンパス |
| 開催地（英） | Tokai Univ.(Takanawa) |
| テーマ（和） | 提案型エンタプライズモデリング ワークショップ |
| テーマ（英） | Enterprise Modeling Workshop |
| 講演論文情報の詳細 | |
| 申込み研究会 | SWIM |
| 会議コード | 2011-11-SWIM |
| 本文の言語 | 日本語 |
| タイトル（和） | 上流設計からモデル検査プロセスまでの一貫設計検証環境 |
| サブタイトル（和） | 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)（和/英） | PROMELA / SPIN |
| キーワード(5)（和/英） | 線形時相論理 / PROMELA |
| キーワード(6)（和/英） | 仕様パターン / Linear Temporal Logic |
| キーワード(7)（和/英） | / Specification Patterns |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 宮本 直樹 / Naoki Miyamoto / ミヤモト ナオキ |
| 第1著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ) |
| 第2著者 氏名（和/英/ヨミ） | 和崎 克己 / Katsumi Wasaki / ワサキ カツミ |
| 第2著者 所属（和/英） | 信州大学 (略称： 信州大) Shinshu University (略称： Shinshu Univ) |
| 講演者 | 第1著者 |
| 発表日時 | 2011-11-18 10:30:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SWIM |
| 資料番号 | SWIM2011-19 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | no.308 |
| ページ範囲 | pp.7-12 |
| ページ数 | 6 |
| 発行日 | 2011-11-11 (SWIM) |
[研究会発表申込システムのトップページに戻る]