| 大会名称 |
|---|
| 2010年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2010 |
| 発行日 |
| 2010/8/20 |
| セッション番号 |
| 4B |
| セッション名 |
| モデル検査・検証・信頼性 |
| 講演日 |
| 2010/09/08 |
| 講演場所(会議室等) |
| B会場（総合学習プラザ1F 第6講義室） |
| 講演番号 |
| B-020 |
| タイトル |
| UML記述の仕様からSPINモデル検査用PROMELAモデルへの自動変換 |
| 著者名 |
| 宮本 直樹, 和崎 克己, |
| キーワード |
| モデル駆動開発, UML, モデル検査, SPIN, PROMELA, 線形時相論理 |
| 抄録 |
| 本研究では，UML図で書かれた上流モデルと要求仕様を，SPINモデル検査器で使用するPROMELA言語コードと時相論理式による仕様に自動変換する方法について検討する．まず，対象オブジェクトについて既存のUMLツールを用いて，複数のステートマシン図と，ステートマシンのインスタンスならびに通信チャネルの関係を記述した配置図としてエントリする．ここで，UMLのステートチャート図には記述の曖昧性が存在するため，特にトランジションと終了状態に関する自由度を制限し，自動変換が容易となるようにした．UMLのデザインエントリ全体を，XML形式でエクスポートされたファイル経由で，PROMELA言語コードへ自動変換する．また，UML記述に仕様パターンを埋め込むことで，線形時相論理式(LTL)へ展開する機能も実現した．自動変換後のPROMELAコードと時相論理式をセットで扱うことで，UMLからモデル検査器までの一貫した設計検証が可能となった． |
| 本文pdf |
| PDF download (210KB) |