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