| 大会名称 |
|---|
| 2010年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2010 |
| 発行日 |
| 2010/8/20 |
| セッション番号 |
| 6E |
| セッション名 |
| マネジメント・モデリング・育成 |
| 講演日 |
| 2010/09/09 |
| 講演場所(会議室等) |
| E会場（総合学習プラザ1F 第9講義室） |
| 講演番号 |
| O-008 |
| タイトル |
| 機能仕様と振る舞い仕様間の整合性 |
| 著者名 |
| 安田 佳宏, 新川 芳行, |
| キーワード |
| UML, 形式手法, モデル検査 |
| 抄録 |
| UML2.0ではシーケンス図に時間を含む制約の記述が可能となっているが, シーケンス図はシステムの動的な振る舞いしか記述できず, 処理の意味的もしくは機能的側面を考慮した制約の記述は困難である. また, UML自体にモデル検証能力がないため, 作成したモデルがこれらの制約を満たすか否かは他のツール等により行う必要がある. 本論文では, 形式仕様記述言語により記述されたクラスの仕様とシーケンス図のマッチングにより導出した, 機能仕様および時間制約を含む時間オートマトンをモデル検査ツールUPPAALにより検証することで, モデルの機能面, 振る舞い面, および時間制約という複数視点からの評価を可能とする手法を提案する. |
| 本文pdf |
| PDF download (546.3KB) |