本文章是由機器翻譯。

模型式測試

模型式測試及規格總管簡介

Sergio Mera
Yiming Cao

生產高品質的軟體要求有作出重大的努力就是在測試中,這可能是軟體發展過程的最昂貴、 最密集的地方之一。有很多途徑提高檢測的可靠性和有效性,從最簡單的功能黑箱測試到重量級方法涉及定理和正式要求規範。然而,測試總是不包括必要的徹底性,水準和紀律和方法往往是缺席。

微軟一直成功地實行基於模型測試 (MBT) 到它的內部發展進程現在超過十年。主戰坦克已被證明成功的技術,為各種內部和外部的軟體產品。通過多年來穩步增加。相對來說,它受到測試社會上,特別是生活在"正式"一側測試頻譜的其他方法相比。

Spec 資源管理器是 Microsoft MBT 工具,它擴展了Visual Studio,為提供一個高度集成的開發環境創建行為模型,再加上檢查這些模型的有效性和生成測試案例從他們的圖形分析工具。我們認為這一工具是引爆點,促進了作為 IT 行業中的一種有效技術 MBT 的應用,減輕自然的學習曲線和提供先進的創作環境。

在這篇文章我們提供背後 MBT 和規範資源管理器中,通過案例研究,來展示它的主要特點提出規範資源管理器中的主要概念的一般概述。我們也希望這篇文章,作為一個實際的經驗法則為了解何時考慮 MBT 作為特定的測試問題的品質保證方法的集合。盲目不應該在每個測試方案中使用 MBT。很多時候另一種技術 (像傳統測試) 可能是更好的選擇。

是什麼讓一個可測試模型規格資源管理器中?

儘管不同的 MBT 工具提供不同的功能,有時有細微的概念差異,有普遍的意義,"做主戰坦克"。基於模型的測試是指從模型自動生成測試程式。

模型都通常手動編寫的包括系統要求和預期的行為。在規範資源管理器中,從面向狀態的模型自動生成測試案例。他們包括測試序列和測試 oracle。測試序列,從模型中,推斷出負責駕駛測試 (SUT) 以達到不同的狀態下的系統。測試 oracle 跟蹤 SUT 的演變,並確定它是否符合指定的模型,發出裁決的行為。

該模型是規範資源管理器中專案中的主要作品之一。它被指定構造調用模型的程式中。您可以在任何.NET 語言 (如 C#) 編寫模型程式。他們包括一組已定義的狀態與交互的規則。模型程式還結合了一種指令碼語言稱為線,規範資源管理器中專案中的第二個關鍵區段。這就允許指定配置的模型是如何探索和測試的行為描述。模型程式和臍帶腳本的組合為 SUT 創建一個可測試模型。

當然,規範資源管理器中專案的第三個重要一塊是 SUT。它不是強制性提供這對規範資源管理器中生成的測試代碼 (這是規範資源管理器預設模式),因為生成的代碼直接從可測試模型中,無需任何交互與 SUT 推斷。您可以執行測試案例"離線"脫鉤模型評價和測試案例生成階段。但是,如果提供 SUT,規範資源管理器中可以驗證從模型到執行的綁定是明確界定。

案例研究:聊天系統

讓我們看一個示例,顯示如何創建一個可測試模型規範資源管理器中的看。在這種情況下 SUT 將會具有單個聊天室,使用者可以登錄和登出的簡單的聊天系統。當使用者登錄時,他可以請求登錄的使用者的清單,並向所有使用者發送廣播的消息。聊天伺服器始終確認請求。請求和回應的行為以非同步方式,意味著他們可以將混在一起。如預期中的聊天系統,不過,按順序接收從一個使用者發送多個消息。

使用 MBT 的優點之一是通過強制執行需要正式確定行為模型,你可以得到很多回饋的要求。歧義、 矛盾和缺乏上下文可以表面在早期階段。所以它是重要的是要準確地和正規化的系統要求,就像這樣:

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 的資源管理器中專案使用操作來描述與從測試系統角度 SUT 的互動。這些行動可以叫用作業,表示一種刺激從測試系統到 SUT ; 返回行動,捕獲的回應 SUT (如果有) ; 和代表自主從 SUT 發送的消息的事件操作。調用/返回操作阻塞操作,所以他們代表由 SUT 中的一個方法。這些都是預設的行動宣言,而"事件"關鍵字,用來聲明事件的操作。圖 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<int> userList);
  action void BroadcastRequest(int senderUser, string message);
  action void BroadcastAck(int receiverUser, 
    int senderUser, string message);
  // ...
}

與聲明的行動下, 一步是定義系統行為。 對於此示例,該模型是使用 C# 進行描述。 與類欄位建模系統狀態和狀態轉換進行建模與規則的方法。 規則的方法確定您可以從目前狀態的模型程式和狀態如何更新的每個步驟中的步驟。

由於此聊天系統基本上包含使用者和系統之間的相互作用,模型的狀態只是一個集合的使用者與他們的國家 (見圖 2)。

圖 2 的模型狀態

/// <summary>
/// A model of the MS-CHAT sample.
/// </summary>
public static class Model
{
  /// <summary>
  /// State of the user.
/// </summary>
  enum UserState
  {
    WaitingForLogon,
    LoggedOn,
    WaitingForList,
    WatingForLogoff,
  }
  /// <summary>
  /// A class representing a user
  /// </summary>
  partial class User
  {
    /// <summary>
    /// The state in which the user currently is.
/// </summary>
    internal UserState state;
    /// <summary>
    /// 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.
/// </summary>
    internal MapContainer<int, Sequence<string>> waitingForDelivery =
      new MapContainer<int,Sequence<string>>();
  }             
    /// <summary>
    /// A mapping from logged-on users to their associated data.
/// </summary>
    static MapContainer<int, User> users = new MapContainer<int,User>();
      // ...   
  }

正如您所看到的定義一個模型的狀態沒有太大不同從定義一個正常的 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<int, Sequence<string>>();
  users[userId] = user;
}

這種方法描述行動"LogonRequest,"以前在電源線代碼中聲明的啟動條件和更新規則。 本質上說,這條規則:

  • 時輸入使用者 Id 尚不存在在當前的使用者集,可以執行的 LogonRequest 操作。 "Condition.Is­真實"是 API 提供的規範資源管理器中用於指定一個有利的條件。
  • 當滿足這一條件時,用其正確初始化的狀態被創建一個新的使用者物件。 它然後添加到全域使用者集合。 這是規則的"更新"部分。

此時,完成建模工作的多數。 現在讓我們定義一些"機器",所以我們可以探索系統的行為,並得到一些視覺化。 規範資源管理器中,機器是勘探的單位。 一台機器有一個名稱和在臍帶語言中定義的相關的行為。 你也可以撰寫一台機器與他人合作,形成更多複雜的行為。 讓我們看看幾個例如機器聊天模型:

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

我們定義的第一個機器是一個所謂的"模型的程式"的機器。 它使用"的構造模型程式"指令來告訴規範資源管理器中,探索基於規則方法發現在 Chat.Model 命名空間中的模型的整個行為:

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

第二台機器是"方案"中以正則運算式類似的方式定義的操作模式。 方案通常由"模型專案"機組成以切片的全部行為,如下所示:

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

"| |"運算子創建"已同步的平行組成"兩個參與機器之間。結果行為將包含的步驟只可以同步這兩台電腦 ("已同步"我們指的是具有相同的操作具有相同的參數清單)。探索這台機器在圖中所示的結果圖 3


圖 3 撰寫的兩台機器

正如你從圖中可以看到圖 3,組成的行為符合方案機和模型程式。這是強大技術獲取的複雜行為的簡單子集。另外,當您的系統具有無限狀態空間 (如聊天系統的情況),切片的全部行為可以生成更適合用於測試目的的有限子集。

讓我們分析在此圖中的不同實體。圈子國家是可控狀態。他們哪裡向 SUT 提供刺激的國家。鑽石的國家有可觀察到的國家。他們是一個或多個事件預計從 SUT 的國家。測試 oracle (測試的預期結果) 已被編碼在事件的步驟和他們的論據的關係圖中。具有多個傳出事件步驟的國家被稱為非確定性的國家,因為該事件 SUT 提供了在執行時間不在建模的時間確定。觀察那中的探索圖圖 3包含幾個非確定性狀態:S19 S20、 S22 等等。

探索的圖是有助於理解系統,但它還不適合的測試,因為它不在"測試正常"表單中。我們說一種行為是在測試正常形式是否它不包含任何具有多個傳出調用返回步驟的狀態。在圖中圖 3,你可以看到 S0 明顯違反了這一規則。若要轉換測試正常表單的這種行為,您只需創建一台新的機器使用的測試案例建設:

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

此構造生成一種新行為通過遍歷的原始行為並在測試正常形式生成的蹤影。遍歷標準是邊緣覆蓋範圍。每個步驟中的原始行為覆蓋至少一次。中的圖圖 4 後這種遍歷顯示行為。


圖 4 生成新的行為

為了實現測試正常形式,具有多個調用返回步驟的國家被拆分為每個步驟之一。事件步驟永遠不分開,總是充分保留,因為事件 SUT 在運行時可以作出的選擇。測試案例必須準備應付任何可能的選擇。

Spec 資源管理器中可以生成測試套件代碼從測試正常表單的行為。生成的測試代碼的預設格式是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 測試案例。

完整的聊天模式列入規範資源管理器中安裝程式。

MBT 還清時?

有利弊時使用基於模型的測試。 最明顯的優點是可測試模型完成後,您可以通過按一個按鈕生成測試案例。 此外,模型已正式到前面的事實可以及早發現的規定不一致之處,可説明團隊在協定的預期行為。 請注意在編寫時手動測試用例,"模式"也是有,但它不正式和生活在測試儀的頭。 主戰坦克部隊測試團隊明確傳達其對系統行為的期望並把它們寫下來使用定義良好的結構。

另一個明顯的優勢是專案維護為低。 更改系統的行為或新添加的功能可以通過更新模型,通常于簡單很多更改手動測試用例,反映出一個接一個。 確定測試案例,需要更改有時是非常耗時的任務。 以及考慮模型創作是獨立的執行或實際的測試。 這意味著可以同時處理不同的任務在不同團隊的成員。

不利的方面,往往需要一種心態的調整。 這可能是這種技術的重大挑戰之一。 在 IT 行業中的人沒有時間去試試新的工具的已知問題,使用這種技術的學習曲線並不是可以忽略不計。 根據團隊,應用 MBT 可能需要一些過程變化,其中還可以生成一些推回。

其他缺點是要做更多的工作提前,所以它需要更多時間來看看正在恒的第一個測試案例­無聲,比使用傳統的手動書面的測試案例。 此外,測試專案的複雜性需要足夠大,說明有理由投資。

幸運的是,有一些經驗法則我們認為説明識別時 MBT 真的不負有心人。 有要求你可以以不同的方式支付系統國家無限集是第一個標誌。 無功或分散式的系統或系統非同步或非確定性相互作用是另一個。 此外,有許多複雜的參數的方法可以指向 MBT 方向。

當滿足這些條件時,MBT 可以作出很大的差別,並保存測試作出重大努力。 一個例子是微軟校樣,作為 Windows 協定遵守倡議的一部分驗證數以百計的協定,在一個專案。 在此專案中,我們可以用規範資源管理器來驗證技術準確性的實際協定行為有關的協定檔。 這是一項巨大努力和微軟花了大約 250 人-­年在測試中的。 微軟研究驗證統計研究顯示使用 MBT 保存 Microsoft 50 個人年測試儀的工作,或努力的 40%左右相比傳統的測試方法。

基於模型的測試是一種強大的技術,將系統方法添加到傳統的技術。 Spec 資源管理器是一個成熟的工具,利用了作為一個免費的Visual Studio電源工具的高度集成的、 先進的發展環境中的 MBT 概念。

Yiming Cao 是協定工程框架 (包括 Microsoft 消息分析儀) 和規範資源管理器中為微軟交互操作和工具團隊和工程的高級發展線索。在加入微軟之前他為 IBM 公司工作 對其企業的協作套件,然後加入關於流媒體技術工作啟動公司。

Sergio Mera  是微軟交互操作和工具團隊和作品的協定工程框架 (包括 Microsoft 消息分析儀) 和規範資源管理器中的高級專案經理。在加入微軟之前他是一位研究員和講師,電腦科學系在布宜諾斯艾利斯大學和工作模態邏輯和自動定理證明。

衷心感谢以下技术专家对本文的审阅: Nico Kicillof (Microsoft)
Nico Kicillof (nicok@microsoft.com) 是主管專案經理為 Windows Phone 構建體系結構和開發工具。 他的工作包括在創建工具和方法,使工程師能夠生成、 測試和維護的軟體產品。 在加入微軟之前, 他是教授和電腦科學系在布宜諾斯艾利斯大學副主席。