著者：早水公二 (株式会社フォーマルテック)、高井利憲 (チェンジビジョン)

みなさん、こんにちは。

2017年7月31日の記事では、ステートマシン図の設計品質の向上のための方法として、モデル検査を紹介しました。今回は、ソフトウェア開発におけるモデル検査の利用例をいくつか紹介します。

前回の記事では、モデル検査の概要とステートマシン図にモデル検査を適用して設計ミスを発見した事例を紹介しました。紹介した事例では、モデル検査のメリットである、

(1) 網羅的な検査ができること

がいかされました。モデル検査のメリットには他にも次のようなものもあります。

(2) モデルと検査式を作成した後の繰り返し試験が容易であること
(3) モデルと反例を共有することで不具合情報を共有できること

今回は、上の(1)(2)(3)のメリットをそれぞれ有効に活用したモデル検査のユースケースをご紹介します。

1. テストフェーズで利用したケース

まずは、最も典型的なユースケースです。システム開発のテストフェーズで、モデル検査を応用して不具合を発見したり除去したりすることにより、品質保証活動を支援します。

□ モデル検査の担当：テスト部門／品質保証部門／（開発部門）
□ 検査目的：不具合の発見・除去、品質保証
□ 検査対象：出荷前のテスト済みのシステム
□ 活用したモデル検査のメリット：(1) 網羅的な検査ができること
□ 結果報告先：開発部門
□ 関係者まとめ

□ 情報の流れのまとめ

□ 活用イメージ

モデル検査を担当するのは、テスト部門や品質保証部門です。開発部門がお手伝いすることも考えられます。場合によっては開発部門が、自らモデル検査を適用して品質を向上させることも有効な手段です。検査対象は開発完了後、単体テストや組合せテスト、総合テストを終えた出荷前のシステムです。モデル検査の最大のメリットである網羅的検査を活用して、従来手法によるテストを実施しても残存しているかもしれない、発生頻度の低いバグや根の深いバグを発見します。

検査の結果は開発部門にフィードバックします。「開発部門でバグの改修 → モデルの改修 → モデル検査で改修の確認」の作業を繰り返して、システムの品質を保証します。

2. 設計フェーズでの品質向上に利用したケース

次は、少し応用的なユースケースです。システム開発の設計フェーズでモデル検査を用いて設計品質の向上を行うケースです。

□ モデル検査の担当：設計者
□ 検査対象：自身の設計内容（ステートマシン図など）
□ 検査目的：

上位仕様との整合性確認
設計内容の矛盾・漏れ・間違いの発見

□ 活用したモデル検査のメリット：(2)モデルと検査式を作成した後の繰り返し試験が容易であること
□ 結果報告先：設計者自身
□ 関係者まとめ

□ 情報の流れのまとめ

□活用イメージ

モデル検査を実施するのは設計者です。検査対象は設計者自身が現在設計しているステートマシン図や、シーケンス図、アクティビティ図等です。設計をしながらモデルも作成していき、適宜、モデル検査を行うことで、現在の設計内容が上位仕様と整合が取れているか、設計内容に矛盾・漏れ・間違いがないか、を確認しながら開発を進めます。モデル検査では、一度、モデルと検査式を作成すれば、ツールを実行（リターンボタンを押す）だけで、何度でも簡単に回帰テストができるので、「設計 → 検証 → 改修 → 確認」の設計と検証のループを繰り返すことで設計品質を向上させることができます。

プロジェクト全体や社内のグループで新しい技術を導入するには、様々な障壁が現れる場合がありますが、この利用方法では、設計者自身の閉じた世界で簡単に始めることができます。

また、設計にステートマシン図やシーケンス図、アクティビティ図を利用していれば、その図からモデルを自動生成するツールを開発すれば、作業時間を大幅に短縮できます。

3. 顧客との仕様検討時に利用したケース

最後は、かなり応用的にモデル検査を利用したケースです。受託システムの開発における初期段階で、モデル検査を用いて要求仕様の確定を行うケースです。

□ モデル検査の担当：受託側企業
□ 検査目的：顧客の要望や希望する仕様の矛盾・漏れ・間違いの発見、仕様確定
□ 検査対象：顧客と検討中の要求仕様書（自然言語＋ステートマシン図）
□ 活用したモデル検査のメリット：(3) モデルと反例を共有することで不具合情報を共有できること
□ 結果報告先：発注側企業（顧客のシステム担当者）
□ 関係者まとめ

□ 情報の流れのまとめ

□ 活用イメージ

モデル検査を実施するのは主として受託側企業の担当者です。顧客のシステム担当者がエンジニアである場合、モデル検査の説明やデモを見て頂くことで興味を持って頂き、検査に参加される場合もあります。検査対象は、顧客と検討中の要求仕様書です。システム開発の最上位のフェーズのドキュメントなので自然言語で書かれている場合が多いですが、複雑なシステムや大規模なシステムでは、ステートマシン図等が記述されている場合もあります。要求仕様書にモデル検査を適用することで、顧客の要望や希望する仕様の矛盾や漏れ、間違いを発見して報告します。その際に、モデル検査ツールにより、モデル及び反例を顧客と共有することで、顧客自身が要望の矛盾・漏れ・間違いを反例上で見ることができます。過去の事例では、モデルを共有したうえで、顧客が自身で作成した検査式でモデル検査を行って、要求仕様の間違いを発見して仕様を改良されたこともありました。このケースでは、モデル検査をコミュニケーションの道具として活用することで、要求仕様の早期確定を行うことができました。また、発注側の企業がモデル検査の有効性を知ることで、モデル検査ができる企業に優先的に発注したり、以後の開発でモデル検査を適用するコストを考慮して頂いたり、さまざまなメリットがあります。

いかがでしたでしょうか。ソフトウェアやシステムの開発にUMLやSysMLなどモデリング言語を利用するメリットの一つには、実装をする前の段階でさまざまな方法で要求や設計の妥当性を確認できることがあげられると思います。モデル検査は、その中でもシミュレーションなどと並ぶツール支援による有力な検証手法の一つです。モデルの活用の手段の一つとして、皆さんの開発現場でもぜひ導入を検討してみてください。