モデル検査を実際の業務に適用する場合,モデル検査の知識や経験を有した人材の不足が問題となる.そこで,著者らは従来の設計ツールであるシーケンス図を用いてモデル検査を可能とするモデル検査支援ツールcsp-seqを開発した.csp-seqは,シーケンス図で記載した内部仕様と外部仕様を,検査モデルと検査仕様にそれぞれ変換することでモデル検査ツールへの入力を作成可能とする.また,モデル検査ツールが出力する反例情報を期待動作と違反動作のシーケンス図に変換し,それらの差分を強調表示することで検査仕様違反の原因特定を容易にする.csp-seqの評価として,業務モデルにcsp-seqを適用し,業務で実際に検出した再現性の低い不具合を,モデル検査に関する知識や経験を必要とせずに効果的に検出できることを確認した.