| 大会名称 |
|---|
| 2010年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2010 |
| 発行日 |
| 2010/8/20 |
| セッション番号 |
| 4B |
| セッション名 |
| モデル検査・検証・信頼性 |
| 講演日 |
| 2010/09/08 |
| 講演場所(会議室等) |
| B会場（総合学習プラザ1F 第6講義室） |
| 講演番号 |
| B-019 |
| タイトル |
| UMLモデルの振舞いのモデル検査における表現方法について |
| 著者名 |
| 八鍬 豊, 野田 夏子, |
| キーワード |
| モデル検査, Spin, Promela, UML, 変換 |
| 抄録 |
|
本稿では，形式手法についての知識を持たないソフトウェア開発者でも モデル検査技術による設計検証を行えるようにすることを目的とし， UMLモデルをモデル検査ツールSPINの入力言語であるPromelaのコードに 変換する方法を提案する．この変換においては，UMLモデルが表現する ソフトウェアの振舞いをいかにPromela言語で表現するかが重要である． また，UMLモデルからPromelaコードへの変換方法を検討する際に 留意すべきPromela仕様を取り上げ，考察を述べる． |
| 本文pdf |
| PDF download (348.7KB) |