モデルベーステスト

[アーティクル]
06/12/2015

モデルベーステストと Spec Explorer の概要

Sergio Mera
Yiming Cao

ソフトウェアの品質を上げるには、テストにかける労力を増やす必要があります。おそらく、ソフトウェア開発プロセスで最もコストと手間がかかるものの 1 つがテストです。テストの信頼性と効率を上げる方法は、機能の単純なブラックボックステストから、定理証明器や形式的要件仕様が必要な複雑な手法までさまざまです。それでも、常に必要なレベルの緻密さが得られるとは限らず、規則や方法論もほとんどありません。

マイクロソフトが社内の開発プロセスにモデルベーステスト (MBT) を導入してから 10 年以上になります。MBT は、社内向けや社外向けのさまざまなソフトウェア製品に有効であることが実証され、導入比率も年々着実に増加しています。相対的に見れば、MBT は特に他の「形式的な」テスト手法と比べて、テストコミュニティに積極的に受け入れられています。

Spec Explorer は Visual Studio を拡張するマイクロソフト製の MBT ツールで、動作モデルを作成するための高度な統合開発環境と、それらのモデルの有効性を確認してテストケースを生成するグラフィカルな分析ツールを提供しています。このツールによって MBT への理解が進み、最新鋭の作成環境が用意されたことで、MBT が有効な手法として、IT 業界での導入増加のきっかけになりました。

今回は、ケーススタディを使って Spec Explorer の機能を紹介しながら、MBT と Spec Explorer を支える主な考え方を大まかに説明します。また、具体的なテストの課題について、どのような場合に品質保証の方法論として MBT の採用を検討すればよいかを理解するための経験則もまとめています。すべてのテストシナリオでむやみに MBT を使用すべきではありません。従来型のテストなど、他の手法が適している場合もよくあります。

Spec Explorer でテスト可能なモデルの条件

MBT ツールはそれぞれ機能が異なり、相反する考え方を採用しているツールもありますが、「MBT を行う」という言葉には共通認識があり、「モデルを基にテスト手順を自動生成すること」を指します。

モデルは通常、手作業で作成し、システム要件と想定する動作を含めます。Spec Explorer の場合、状態指向のモデルからテストケースを自動生成します。生成されるテストケースには、テストシーケンスとテストオラクル (テストの想定結果) の両方が含まれます。テストシーケンスはモデルから推測され、テスト対象システム (SUT) をさまざまな状態に導く役割があります。テストオラクルは、SUT の変化を追跡し、モデルで指定された動作に従っているかどうかを判断します。

モデルは Spec Explorer プロジェクトの主要要素の 1 つで、モデルプログラムという構造で指定します。これは、任意の .NET 言語 (C# など) で記述でき、定義した状態を操作する一連のルールで構成します。モデルプログラムは Cord というスクリプト言語と組み合わせて使用します。Cord は Spec Explorer プロジェクトの 2 つ目の主要要素です。Cord により、モデルの探索方法とテスト方法を構成する動作の説明を指定できるようになります。モデルプログラムと Cord スクリプトを組み合わせることで、SUT のテスト可能なモデルを作成します。

当然、Spec Explorer プロジェクトの 3 つ目の主要要素は SUT です。生成されるコードは SUT を操作しなくてもテスト可能なモデルから直接推測されるため、テストコードの生成時に SUT を Spec Explorer に指定する (Spec Explorer 既定のモード) のは必須ではありません。テストケースは、モデルの評価段階やテストケースの生成段階とは切り離して、"オフライン" で実行できます。ただし、SUT を指定しておけば、Spec Explorer はモデルから実装へのバインドが適切に定義されているかどうかを検証できます。

ケーススタディ: チャットシステム

Spec Explorer でテスト可能なモデルを構築する方法の一例を見てみましょう。今回の SUT は、単純なチャットシステムで、ユーザーがログオン/ログオフできるチャットルームが 1 つだけあります。ユーザーは、ログオンすると、現在ログオン中のユーザーのリストを要求し、すべてのユーザーにブロードキャストメッセージを送信できます。チャットサーバーは常に要求に対して確認応答を返します。要求と応答は非同期に行われるため、入り混じることがありますが、チャットシステムとしては当然、一人のユーザーが送信した複数のメッセージは、相手に順番どおりに届きます。

MBT を使用するメリットの 1 つは、動作モデルを必ず形式化しなければならないため、要件に対して多くのフィードバックを得られるようになることです。要件のあいまいさ、矛盾、コンテキスト不足などは早い段階で表面化します。そのためにも、システム要件を細かく形式化することが重要です。以下に例を示します。

R1. Users must receive a response for a logon request.
 R2. Users must receive a response for a logoff request.
 R3. Users must receive a response for a list request.
 R4. List response must contain the list of logged-on users.
 R5. All logged-on users must receive a broadcast message.
 R6. Messages from one sender must be received in order.

Spec Explorer プロジェクトでは、アクションを使用して、テストシステムの観点から SUT との対話を記述します。アクションには、テストシステムから SUT に働きかける呼び出しアクション、SUT からの応答をキャプチャするリターンアクション、および SUT から送信される自発的なメッセージを表すイベントアクションがあります。呼び出しアクションとリターンアクションはブロック操作になるため、SUT では単一のメソッドとして表現します。呼び出しアクションとリターンアクションは既定のアクション宣言ですが、イベントアクションの宣言には "event" キーワードを使用します。図 1に今回のチャットシステムにおけるアクションの例を示します。

図 1 アクションの宣言

// Cord code
 config ChatConfig
 {
   action void LogonRequest(int user);
   action event void LogonResponse(int user);
   action void LogoffRequest(int user);
   action event void LogoffResponse(int user);
   action void ListRequest(int user);
   action event void ListResponse(int user, Set userList);
   action void BroadcastRequest(int senderUser, string message);
   action void BroadcastAck(int receiverUser, 
     int senderUser, string message);
   // ...
 }

アクションを宣言したら、次はシステムの動作を定義します。今回の例では、モデルを C# で記述しています。システムの状態はクラスのフィールドを使ってモデル化し、状態遷移はルールのメソッドを使ってモデル化します。ルールのメソッドは、モデルプログラムでの現在状態から得られる手順と、各手順で状態を更新する方法を決定します。

今回のチャットシステムは基本的にユーザーとシステムとの対話で構成されるため、モデルの状態は単にユーザーとその状態のコレクションです (図 2 参照)。

図 2 モデルの状態

/// 
 /// A model of the MS-CHAT sample.
 /// 
 public static class Model
 {
   /// 
   /// State of the user.
   /// 
   enum UserState
   {
     WaitingForLogon,
     LoggedOn,
     WaitingForList,
     WatingForLogoff,
   }
   /// 
   /// A class representing a user
   /// 
   partial class User
   {
     /// 
     /// The state in which the user currently is.
     /// 
     internal UserState state;
     /// 
     /// The broadcast messages that are waiting for delivery to this user.
     /// This is a map indexed by the user who broadcasted the message,
     /// mapping into a sequence of broadcast messages from this same user.
     /// 
     internal MapContainer&gt; waitingForDelivery =
       new MapContainer&gt;();
   }             
     /// 
     /// A mapping from logged-on users to their associated data.
     /// 
     static MapContainer users = new MapContainer();
       // ...   
   }

ご覧のとおり、モデルの状態の定義は、通常の C# クラスの定義とほとんど変わりません。ルールのメソッドは、アクションをアクティブにできる状態を記述する C# メソッドです。また、アクションがアクティブになったときに、モデルの状態がどのように更新されるかも記述します。ここで、ルールのメソッドの記述方法を説明する例として、"LogonRequest" を示します。

[Rule]
 static void LogonRequest(int userId)
 {
   Condition.IsTrue(!users.ContainsKey(userId));
   User user = new User();
   user.state = UserState.WaitingForLogon;
   user.waitingForDelivery = new MapContainer&gt;();
   users[userId] = user;
 }

このメソッドでは、先ほど Cord コードで宣言したアクション "LogonRequest" のアクティブ化条件と更新のルールを記述しています。このルールを要約すると、次のとおりです。

LogonRequest アクションは、入力された userId が現在のユーザーセットにまだ存在しない場合に実行できます。"Condition.IsTrue" は、Spec Explorer が提供する API で、有効化する条件を指定します。
この条件が満たされると、状態を適切に初期化した状態で新しい user オブジェクトを作成し、グローバル users コレクションに追加します。これがルールの "更新" 部分です。

この時点で、モデル化作業の大半は終了です。次に、システムの動作を探索して視覚化するための "マシン" (machine) を定義します。Spec Explorer では、マシンが探索の単位です。マシンには、名前とマシンに関連付けられた動作があり、Cord 言語で定義します。また、マシンを複数組み合わせて、複雑な動作を構成することもできます。チャットモデルのマシンの例をいくつか見てみましょう。

machine ModelProgram() : Actions
 {
   construct model program from Actions where scope = "Chat.Model"
 }

最初に定義するマシンは "モデルプログラム" マシンです。このマシンは、Chat.Model 名前空間にあるルールのメソッドに基づいて、モデルの全体的な動作を探索するよう "construct model program" ディレクティブを使用して Spec Explorer に指示しています。

machine BroadcastOrderedScenario() : Actions
 {
   (LogonRequest({1..2}); LogonResponse){2};
   BroadcastRequest(1, "1a");
   BroadcastRequest(1, "1b");
   (BroadcastAck)*
 }

2 つ目のマシンは "シナリオ" です。正規表現のような方法でアクションのパターンを定義しています。シナリオは通常、すべての動作を切り分けるために、"モデルプログラム" マシンと組み合わせます。次にその例を示します。

machine BroadcastOrderedSlice() : Actions
 {
   BroadcastOrderedScenario || ModelProgram
 }

"||" 演算子により、参加している 2 つのマシン間の "同期並列構成" を作成します。最終的な動作には、両方のマシンで同期可能な手順のみが含まれます ("同期" とは同じ引数リストが設定された同じアクションを意味します)。このマシンを探索すると、図 3 のグラフのようになります。

図 3 2 つのマシンの組み合わせ

図 3のグラフに示すように、組み合わせた動作はシナリオマシンにもモデルプログラムにも基づいています。これは、複雑な動作から単純なサブセットを得る有効な手段です。また、システムに無限の状態空間がある場合 (チャットシステムの場合など)、すべての動作を切り分けることでテスト目的に適した有限サブセットを生成できます。

このグラフのさまざまなエンティティを分析してみましょう。円で示している状態は制御可能な状態です。これは、SUT に働きかる状態です。ひし形で示している状態は監視可能な状態です。これは、SUT から 1 つ以上のイベントが想定される状態です。テストオラクル (テストの想定結果) は、イベント手順およびその引数と一緒に既にグラフにエンコードされています。複数のイベント手順に分岐する状態は非決定的状態と呼ばれます。これは、モデル化するときに、SUT の実行時に発生するイベントが決定しないためです。図 3 の探索グラフには、S19、S20、S22 など、非決定的状態がいくつか含まれています。

探索グラフはシステムを理解するのには便利ですが、"テスト標準" 形式ではないため、テストにはまだ適しません。どの状態にも外向きの呼び出し - リターンの手順が 1 つだけの場合に、動作がテスト標準形式になっているといえます。図 3 のグラフでは、S0 が明らかにこのルールに反していることがわかります。このような動作をテスト標準形式に変換するには、テストケース構造を使用して新しいマシンを作成するだけです。

machine TestSuite() : Actions where TestEnabled = true
 {
   construct test cases where AllowUndeterminedCoverage = true
   for BroadcastOrderedSlice
 }

この構造により、元の動作がトラバースされ、テスト標準形式のトレースが生成されて、新しい動作が生成されます。トラバースの基準はエッジカバレッジです。元の動作の各手順は最低 1 回新しい動作に組み込まれます。図 4のグラフは、このようなトラバースを行った後の動作を示しています。

図 4 新しい動作の生成

テスト標準形式にするには、複数の呼び出し - リターン手順がある状態を、手順ごとに 1 つになるよう分割します。イベントは SUT によって実行時に選択されるものなので、イベント手順は分割せず、必ずそのまま残します。選択される可能性があるものすべてに対処するよう、テストケースを準備する必要があります。

Spec Explorer はテスト標準形式の動作からテストスイートコードを生成できます。生成されるテストコードの既定の形式は、Visual Studio 単体テストです。このようなテストスイートは直接 Visual Studio テストツールから実行することも、mstest.exe コマンドラインツールから実行することもできます。生成後のテストコードは、人間に理解できる形式になっているため、簡単にデバッグできます。

#region Test Starting in S0
 [Microsoft.VisualStudio.TestTools.UnitTesting.TestMethodAttribute()]
 public void TestSuiteS0() {
   this.Manager.BeginTest("TestSuiteS0");
   this.Manager.Comment("reaching state \'S0\'");
   this.Manager.Comment("executing step \'call LogonRequest(2)\'");
   Chat.Adapter.ChatAdapter.LogonRequest(2);
   this.Manager.Comment("reaching state \'S1\'");
   this.Manager.Comment("checking step \'return LogonRequest\'");
   this.Manager.Comment("reaching state \'S4\'");
   // ...
     }

テストコードジェネレーターは細かくカスタマイズでき、NUnit などの別のテストフレームワークを対象としたテストケースを生成するように構成することもできます。

完全な Chat モデルは Spec Explorer インストーラーに含まれています。

MBT が効果的になる場合

モデルベーステストにはメリットとデメリットがあります。最も明らかなメリットは、テスト可能なモデルが完成したらボタンを押すだけでテストケースを作成できることです。さらに、あらかじめモデルの形式化が必要なことは、要件の矛盾の早期発見につながり、また、想定される動作に関するチームの認識を一致させるのに役立ちます。手動テストケースを記述する場合にも "モデル" は存在します。ただし、これは形式化されておらず、テスト担当者の頭の中にしかありません。MBT を使用することで、テストチームはシステムの動作の観点から想定を明確に伝達し、適切に定義された構造で記述することを余儀なくされます。

もう 1 つの明確なメリットは、プロジェクトのメンテナンスが少ないことです。システム動作の変更や新しく追加された機能は、モデルを更新することで反映できるため、手動テストケースを 1 つずつ変更するよりも通常格段に簡単です。変更が必要なテストケースだけを特定するのは、時間のかかる作業になることがあります。また、モデル作成は実装や実際のテストとは関係がありません。そのため、チームのメンバーがそれぞれ別の作業に同時に取り組むことができます。

デメリットは、思考の調整が頻繁に必要になることです。これは、おそらくこの手法の大きな課題の 1 つです。新しいツールに取り組む時間が取れないという IT 業界の有名な問題に加え、この手法を理解するまでの時間は無視できません。チームによっては、MBT を使用するときにプロセスの変更が必要な場合もあり、反対を受ける可能性もあります。

もう 1 つのデメリットは、事前の作業が増えるため、従来の手作業で記述するテストケースに比べ、最初のテストケースを生成するまでの時間が長くなることです。また、テストプロジェクトを作成する労力に見合う複雑さも必要です。

さいわい、MBT を効果的に利用できる場合の特定に役立つ経験則がいくつかあります。無限のシステム状態に複数の方法で対応できる要件があることが最初の目印です。事後対応型システムか分散システムか、または同期対話をサポートするシステムか非同期対話をサポートするシステムかは別問題です。ほかにも、複数の複雑なパラメーターを受け取るメソッドは MBT に向いています。

これらの条件に当てはまる場合に MBT を使用すると、大きな効果を発揮し、テスト作業を大幅に削減できます。この例が Microsoft Blueline という、Windows プロトコル遵守イニシアチブの一環として何百ものプロトコルが検証されたプロジェクトです。このプロジェクトで、マイクロソフトは Spec Explorer を使用して、実際のプロトコルの動作についてプロトコルドキュメントの技術的正確性を検証しました。これには多大な労力が必要で、テストに約 250 人年かかりました。Microsoft Research は、マイクロソフトでは MBT を使用することで従来のテストアプローチに比べ、テスト担当者の作業 50 人年分 (労力の約 40%) が削減されたという統計研究を実証しています。

モデルベーステストは従来の手法に体系的な方法論を追加する強力な手法です。Spec Explorer は最新鋭の高度な統合開発環境で MBT の考え方を利用できる成熟したツールでありながら、Visual Studio Power Tool として無料で提供されています。

Yiming Cao はマイクロソフトの相互運用とツールチームのシニア開発担当者であり、プロトコルエンジニアリングフレームワーク (Microsoft Message Analyzer を含む) と Spec Explorer に携わっています。IBM でエンタープライズコラボレーションスイートに取り組んだ後、新興企業でのメディアストリーミングテクノロジの担当を経て、マイクロソフトに入社しました。

Sergio Mera はマイクロソフトの相互運用とツールチームのシニアプログラムマネージャーであり、プロトコルエンジニアリングフレームワーク (Microsoft Message Analyzer を含む) と Spec Explorer に携わっています。ブエノスアイレス大学のコンピューターサイエンス学科の研究者と講師を務め、様相論理学と自動定理証明を研究した後、マイクロソフトに入社しました。

この記事のレビューに協力してくれた技術スタッフの Nico Kicillof (マイクロソフト) に心より感謝いたします。
Nico Kicillof (nicok@microsoft.com、英語のみ) は Windows Phone 構築アーキテクチャとツール開発のリードプログラムマネージャーです。ソフトウェア製品の構築、テスト、および保守をエンジニアが簡単に行えるツールやメソッドを作成するのが仕事です。ブエノスアイレス大学のコンピューターサイエンス学科の教授と副学部長を務めた後、マイクロソフトに入社しました。