| 大会名称 |
|---|
| 2010年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2010 |
| 発行日 |
| 2010/8/20 |
| セッション番号 |
| 4B |
| セッション名 |
| モデル検査・検証・信頼性 |
| 講演日 |
| 2010/09/08 |
| 講演場所(会議室等) |
| B会場（総合学習プラザ1F 第6講義室） |
| 講演番号 |
| B-017 |
| タイトル |
| 時間制約を持つ仕様に対するUML/SysMLモデルの動的検査手法 |
| 著者名 |
| 小野 康一, 河原 亮, 中村 宏明, 石川 浩, |
| キーワード |
| 動的検証, 実行トレース, MARTE, 組込みシステム, リアルタイムシステム, UML |
| 抄録 |
| 時間制約による仕様に対して，UML/SysML による実行可能なシステム・モデルの振舞が整合するかどうかを動的に検査する技術を提案する．制御系の離散的振舞と機械系/電気系の連続的振舞の連携を必要とすることが多い組込みシステム/リアルタイムシステムのモデルでは，制御系のモデルを形式手法などで静的に検証するだけでは不十分であり，動的検査が必要となる．また，開発早期において分析レベル・モデルを用いて性能などの非機能要件の充足性を判断するのにこの検査技術は特に有効である．仕様は，時間制約を付与したシーケンス図の集合で定義する．動的検査は，システム・モデルの実行トレースとして取得するモデル・イベントの列を，シーケンス図に表現されるイベント・パターンおよび制約条件の集合と照合する問題として実現することができる．シーケンス図の集合をイベント・パターンの相違に対応した二分木の集合にあらかじめ変換しておくことで，モデル実行の迅速な検査や，長時間に亘る大量の実行トレースからの仕様との不整合箇所の発見が可能になる． |
| 本文pdf |
| PDF download (724.7KB) |