時間制約による仕様に対して，UML/SysML による実行可能なシステム・モデルの振舞が整合するかどうかを動的に検査する技術を提案する．制御系の離散的振舞と機械系/電気系の連続的振舞の連携を必要とすることが多い組込みシステム/リアルタイムシステムのモデルでは，制御系のモデルを形式手法などで静的に検証するだけでは不十分であり，動的検査が必要となる．また，開発早期において分析レベル・モデルを用いて性能などの非機能要件の充足性を判断するのにこの検査技術は特に有効である．仕様は，時間制約を付与したシーケンス図の集合で定義する．動的検査は，システム・モデルの実行トレースとして取得するモデル・イベントの列を，シーケンス図に表現されるイベント・パターンおよび制約条件の集合と照合する問題として実現することができる．シーケンス図の集合をイベント・パターンの相違に対応した二分木の集合にあらかじめ変換しておくことで，モデル実行の迅速な検査や，長時間に亘る大量の実行トレースからの仕様との不整合箇所の発見が可能になる．
By: 小野康一、河原亮、中村宏明、石川浩
Published in: RT0902 in 2010
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .