大資料/質量驗證的實用 DevOps
系統正確性的分析對於生產執行時行為保證正確的系統至關重要。然而，正確性的概念很普遍，需要根據嵌入該系統的特定場景進行細化。為此，需要考慮適當的標準來定義什麼是正確性，這取決於所考慮的系統型別以及已實現系統在執行時應該表現出來的使用者需求。DICE 中的驗證旨在為 DIA 定義一個可能的正確性含義，並提供支援正式分析的工具。
DICE 中可用於 DIA 安全分析的工具是 D-VerT。DICE 中的安全驗證用於檢查 DIA 模型中是否可以到達不希望的配置，即故障，這包括不符合質量工程師指定的一些非功能性需求的行為。
驗證旨在關注對不正確設計的時間約束效果的分析，這些約束可能會導致資料處理延遲。因此，設計人員可以使用分析工具推斷出反映在驗證結果上的不希望行為的原因。
時間約束的設計是軟體設計的一個方面，在 DICE 中考慮的應用程式中非常重要。不可預見的時間延遲實際上會導致系統出現不正確的行為，這些行為可能以各種形式在執行時出現，具體取決於正在開發的應用程式型別。低估節點的計算能力會影響節點處理輸入資料所需的時間，而這反過來又可能影響整個應用程式的時間跨度，因為處理延遲可能會引發連鎖反應。例如，在流式應用程式中，節點的緩慢可能會導致訊息在佇列中累積，並可能導致記憶體飽和，除非有程式採取措施處理異常。在批處理應用程式中，不可預見的時間延遲可能會影響總處理時間並改變應用程式行為，從而違反與客戶的服務等級協議。
據作者所知，目前還沒有可用的工具提供專門針對 DICE 參考技術開發的這些特殊功能。
DICE 採用 模型檢查 技術來驗證在 DTSM 圖表中指定的 DIA。驗證問題由 DIA 的正式描述（一個包含有關正在分析的應用程式的時間特性的適當資訊的帶註釋的 DTSM 模型）和表示其執行必須滿足的屬性的邏輯公式來指定。
DICE 中的驗證過程依賴於基於稠密時間時態邏輯的完全自動過程，並且它是根據有界模型檢查方法實現的。它被設計為以敏捷的方式進行：DIA 設計師使用輕量級方法執行驗證。更準確地說，D-VerT 鼓勵一種方法，在這種方法中，正式驗證透過隱藏底層模型和引擎複雜性的介面啟動。這些介面允許使用者輕鬆生成要驗證的正式模型以及要檢查的屬性，並消除對正式驗證技術的專家的需求。
驗證結果用於在設計時細化應用程式模型，以防 D-VerT 檢測到異常（參見 用例）。
驗證過程包括以下步驟。設計人員在 DICE IDE 中繪製一個類圖，表示 DIA 的 DTSM 模型，然後根據她用來實現應用程式的所選技術提供分析所需的所有註釋。當用戶開始分析時，帶註釋的 DTSM 模型將轉換為正式模型，該模型表示應用程式在執行時的抽象行為。根據要實現的系統型別 - 無論是 Storm 應用程式還是 Spark 應用程式 - 該工具選擇要驗證的屬性類別並執行分析。最後，當結果可用時，使用者請求 D-VerT 在 DICE IDE 中顯示結果，以檢視屬性是否滿足，如果未滿足，則顯示違反該屬性的系統跟蹤。圖 1 顯示了 D-VerT 工作流程的主要步驟：透過 DICE IDE 建立應用程式的 UML DTSM 模型，從 UML 模型到正式模型的自動轉換，以及實際的執行驗證任務。
如圖 2 所示，D-VerT 採用客戶端-伺服器架構：客戶端元件是一個與 DICE IDE 完全整合的 Eclipse 外掛，伺服器元件是一個 RESTful Web 伺服器。客戶端元件管理從使用者定義的 DTSM 模型到中間 JSON 物件的轉換，然後使用該物件呼叫伺服器。伺服器元件根據 JSON 檔案的內容生成正式模型，然後將其提供給核心可滿足性/模型檢查 工具。此工具負責驗證屬性是否針對提供的公式整合立，即系統的正式模型。
工具的可用性取決於某些非功能性指標的數值估計的可用性，這些指標是D-VerT使用者在標註經過驗證的DTSM模型時需要的。這些值可以透過監測平臺收集執行應用程式（其DTSM模型是從已實施的解決方案中提取出來的）的事件來收集，或者可以透過設計師的經驗或透過從與分析中的應用程式類似的其他應用程式先前收集的歷史資料來估計。
應用領域
[edit | edit source]當前版本的D-VerT支援
在Storm拓撲的情況下，瓶頸分析幫助設計師發現瓶頸節點，因為它們的計時特性設計不正確。計時約束的錯誤設計實際上會導致異常，例如（i）處理元組的延遲和（ii）佇列佔用量的單調增長。
在Spark作業的情況下，可行性分析旨在檢查是否存在一個執行，其持續時間低於特定截止時間，從而證明這種執行的可行性，而有界性分析檢查（對應用程式的空閒時間做出強假設）系統的所有可能執行是否低於某個閾值。
大多數流和批處理參考技術可以透過表示應用程式執行的計算的圖形來描述應用程式。雖然在某些情況下，這些圖形可以從以宣告性方式定義的應用程式中派生（例如，在 Apache Spark 和 Apache Flink 中），但其他技術，例如 Apache Storm 和 Apache Samza，允許直接指定應用程式的拓撲結構，因此可以透過組合多個計算塊以組合的方式定義應用程式。
Storm
[edit | edit source]透過實現應用程式的拓撲結構，在DTSM級別指定Storm應用程式。拓撲結構是一個由兩類節點組成的圖形。
- 輸入節點（噴口）是資訊的來源，它們在定義應用程式邏輯方面沒有任何作用。它們可以透過與注入拓撲的資料流相關的資訊來描述，並且它們的計算特徵與定義拓撲的最終結果無關。
- 計算節點（螺栓）詳細說明輸入資料併產生結果，這些結果反過來被髮射到拓撲結構的其他節點。瓶頸分析僅關注螺栓。
此外，拓撲結構精確地定義了節點之間的連線，節點間通訊基於訊息交換（訊息稱為元組）。因此，對於任何節點n，在設計時（DTSM模型）靜態地定義訂閱n的節點列表（即接收其發射的訊息）和n訂閱的節點列表。
D-VerT使用者需要以下概念（和引數）來執行驗證。
螺栓的行為由五個不同狀態空閒、執行、獲取、發射、失敗的序列定義，其含義如下
- 空閒：目前沒有元組在螺栓中處理。
- 執行：至少有一個但最多Takemax個元組目前正在螺栓中詳細說明。
- 發射：螺栓將元組發射到所有訂閱的螺栓。
- 獲取：螺栓從佇列中獲取至少一個但最多有限數量的元組（由以下並行度值定義），並初始化適當數量的併發執行緒來處理所有這些元組。
- 失敗：螺栓失敗，任何先前狀態都無法發生。
每個螺栓都有以下引數
- σ是一個正實數，它抽象了螺栓計算的功能。如果螺栓過濾元組，即傳入元組的數量大於傳出元組的數量，則0 < σ < 1，否則其值為σ ≥ 0。它表示輸入流和輸出流大小之間的比率。
- 並行度是噴口/螺栓中可能例項化的併發執行緒的最大數量。因此，一個活動的噴口/螺栓可以同時從其佇列中發射/刪除數量等於並行度值的元組。
- α是一個正實數，它表示螺栓處理一個元組所需的時間量。
- 重啟時間（最小/最大）是一個正實數，它表示螺栓在失敗後恢復其功能所需的時間量。
- 空閒時間（最大）是一個正實數，它表示螺栓可能處於空閒狀態的時間量。
- 故障時間（最小）是一個正實數，它表示兩次連續故障之間的時間量。
每個噴口由注入拓撲結構的元組的平均發射速率描述。
Spark
[edit | edit source]透過操作資料的有向無環圖 (DAG)，在 DTSM 級別指定 Spark 應用程式，這些資料在稱為階段的節點中進行聚合。
Spark 中的基本資料結構是所謂的彈性分散式資料集 (RDD)。RDD 支援兩種型別的操作
- 轉換是對 RDD 執行的操作（例如，對映、過濾、連線、聯合等等），這些操作會產生一個新的 RDD。
- 操作是對 RDD 執行的操作（例如，規約、計數、第一個等等），這些操作會返回透過在 RDD 上執行計算獲得的值。
Spark 透過以適當的方式排程其操作來安排轉換，以最大限度地提高並行執行的運算元量。階段是並行地在資料許多分割槽上執行的一系列轉換，這些轉換通常以混洗操作結束。每個階段都是一個計算實體，一旦其所有組成操作完成，就會產生結果。每個階段包含執行階段轉換的許多工；任務是單個數據分割槽上執行的計算單元。
DAG 實現的計算稱為作業。因此，DAG 透過指定操作工作流來定義Spark作業的功能，該工作流指定操作 RDD 的階段之間的依賴關係。兩個階段之間的依賴關係是優先關係；因此，只有在所有前驅階段完成計算後才能執行一個階段。
在執行時，實際的計算是透過工作器、執行器和任務在節點叢集上實現的。工作器是能夠在叢集中執行應用程式程式碼的節點，它包含一些執行器，即執行任務並可能在工作器節點上儲存資料的程序。
D-VerT使用者需要以下概念（和引數）來執行驗證。
- 延遲是每個資料分割槽的任務持續時間的估計，並且
- Tot_cores是執行任務的 CPU 核心數量。
- Tot_tasks是要執行的任務總數
- 截止時間是Spark應用程式的最大持續時間。
可以執行的分析如下
- Spark作業的可行性分析驗證是否存在一個執行，其持續時間低於截止時間；
- 有界性分析檢查系統的所有可能執行是否低於截止時間。
測試用例 - DigitalPebble 網路爬蟲
[edit | edit source]D-VerT 是一個可以在 DICE IDE 中執行的 Eclipse 外掛。為了執行正式驗證任務，需要分別使用 UML 類圖和活動圖來指定 Storm 拓撲和 Spark 作業，並使用 DICE::Storm 和 DICE::Spark 配置檔案進行方便地註釋。可以使用 DICE 工具欄中的 Eclipse 專案進行拖放來輕鬆繪製圖表，而註釋可以在 DICE IDE 的底部面板中指定。
圖 3 描述了實現 DigitalPebble 網頁爬蟲 的 Storm 拓撲。每個節點（無論是 spout 還是 bolt）都已使用執行瓶頸分析所需的引數值進行註釋。
D-VerT 可以透過執行配置視窗設定，允許使用者啟動分析。使用者可以指定的引數如下：
- 包含正在進行分析的模型的檔案。
- 時間邊界限制瞭解決器在拓撲分析中考慮的執行長度。由於 D-VerT 基於有界 模型檢查 方法，因此時間邊界是解決器可以用來生成拓撲執行的最大不同連續事件數。
- 分析中要使用的求解器外掛。
- 要分析的受監控螺栓集。
- D-VerT 伺服器執行的 IP 地址和埠。
分析允許檢測系統可能的執行情況，導致至少一個螺栓佇列的無限增長。如果 D-VerT 檢測到問題，它將返回一個跟蹤，證明了這種系統執行的存在——即違反有界屬性的反例。跟蹤以文字格式（即底層求解器的裸輸出）和圖形格式返回給使用者。圖 4 顯示了這種輸出跟蹤的示例。它表示螺栓佇列中元組數量隨時間的變化。跟蹤由字首和字尾組成：字尾用灰色背景突出顯示，捕獲佇列大小的增長趨勢，因為它對應於系統中可以無限次重複的一系列操作。如果未檢測到跟蹤，則結果為 UNSAT。
圖 5 顯示了實現 WordCount 應用程式的 Spark DAG。
D-VerT 向用戶顯示的執行配置對話方塊允許他們選擇要執行的分析型別（可行性或有界性），以及定義要使用的模型以及伺服器 IP 和埠的引數。
Spark 分析返回布林結果（是/否），指定屬性是否被違反。否定響應附帶了一個反例，證明了違反。
結論
[edit | edit source]DICE 中驗證的主要成就是開發了抽象模型來支援 Apache Storm 和 Spark 應用程式的安全驗證。這些模型是透過邏輯方法構建的。它們被設計為可配置的，並提供了一個分層結構，透過將驗證層與模型 DTSM 圖表分離，從而簡化了與 DICE 框架的整合。開發了特定於模型的模型到模型轉換，以從使用者設計中獲得可驗證模型，後者透過 DICE IDE 中的驗證工具包實現。