B-017 時間制約を持つ仕様に対するUML/SysMLモデルの動的検査手法(B分野:ソフトウェア,一般論文)

• 小野, 康一

• 河原, 亮

• 中村, 宏明

• 石川, 浩

書誌事項

タイトル別名

• B-017 A Dynamic Verification Method of UML/SysML Models with Timed Constraints

抄録

UML/SysMLによる実行可能なシステム・モデルの振舞が,時間/機能制約による仕様に対して整合するかどうかを動的に検査する技術を提案する.制御系の離散的振舞と機械系/電気系の連続的振舞の連携を必要とすることが多い組込みシステム/リアルタイムシステムのモデルでは,制御系のモデルを形式手法などで静的に検証するだけでは不十分であり,動的検査が必要となる.また,開発早期において分析レベル・モデルを用いて性能などの非機能要件の充足性を判断するのにこの検査技術は特に有効である.仕様は,時間/機能制約を付与したシーケンス図の集合で定義する.動的検査は,システム・モデルの実行トレースとして取得するモデル・イベントの列を,シーケンス図に表現されるイベント・パターンおよび制約条件の集合と照合する問題として実現することができる.シーケンス図の集合をイベント・パターンの相違に対応した二分木の集合にあらかじめ変換しておくことで,モデル実行の迅速な検査や,長時間に亘る大量の実行トレースからの仕様との不整合箇所の発見が可能になる.

収録刊行物

• 情報科学技術フォーラム講演論文集

  情報科学技術フォーラム講演論文集 9 (1), 299-306, 2010-08-20

  FIT(電子情報通信学会・情報処理学会)運営委員会

詳細情報

• CRID: 1050855522069007360
• NII論文ID: 110008145580
• NII書誌ID: AA1242354X
• Web Site: http://id.nii.ac.jp/1001/00149845/
• 本文言語コード: ja
• 資料種別: conference paper
• データソース種別:
  • IRDB
  • CiNii Articles