大資料實用 DevOps/跟蹤檢查
跟蹤檢查是一種方法，用於分析記錄為帶時間戳事件序列的系統執行。分析收集的日誌以確定系統日誌是否滿足屬性，通常在邏輯語言中指定。在肯定的情況下，取樣的系統行為符合屬性建模的約束；反之，系統行為 simply does not satisfy the property.
當用於指定屬性的語言允許使用時間運算子時，跟蹤檢查是檢查系統中發生的事件順序以及事件對之間的時間延遲的正確性的一種方法。例如，如果屬性要求某個節點的所有發射事件發生的時間不晚於最新的接收事件的十毫秒，那麼在跟蹤上檢查屬性會導致布林結果，如果兩個連續且有序的發射和接收事件對之間的距離小於十毫秒，則該結果為肯定。
DICE 中可用於執行跟蹤檢查（Storm 應用程式）的工具是DICE-TraCT。
當從監控系統獲得的聚合資料不足以得出系統執行相對於某些特定標準的正確性時，跟蹤檢查特別有用。實際上，在某些情況下，這些標準是依賴於應用程式的，因為它們與應用程式本身的一些非功能屬性相關，並且它們不依賴於應用程式執行的物理基礎設施。
跟蹤檢查是一種可以實現此目標的可能技術，可以有意地用於從正在執行的應用程式的執行中提取資訊。
涉及跟蹤檢查分析的邏輯語言通常是度量時間邏輯的擴充套件，它們提供稱為聚合模態的特殊運算子。如果跟蹤滿足特定的量化特徵，例如跟蹤中事件的特定計數屬性，則這些運算子成立。
根據 DICE 願景，跟蹤檢查在驗證之後執行，以允許持續的模型細化。透過日誌分析獲得的結果確認或反駁了驗證任務的結果，該驗證任務在設計時執行。設計時模型中的引數值與執行時值進行比較；如果兩者都是“相容的”，那麼驗證的結果有效，否則必須細化模型。
與執行時驗證相關的研究領域在跟蹤檢查方面非常活躍。支援跟蹤檢查並提供線上或離線分析的工具多種多樣。DICE 中的跟蹤檢查是離線應用的，但框架的進一步擴充套件可能會考慮線上分析，以改進設計師可以執行的模型驅動細化。據團隊所知，DICE 是（之一）第一個將跟蹤檢查分析用於支援 DIA 模型驅動開發的嘗試。跟蹤檢查引擎是可以在評估過程中使用的工具，選擇特定引擎取決於設計師想要實現的分析型別。The 國際執行時驗證競賽 是比較可用工具和技術的最佳參考。以下是一些參與競賽的工具，可以被視為 DICE 中使用和實現的工具的替代方案
- Rithm2 (論文): 用於驗證具有擴充套件版本的 LTL 的日誌跟蹤的有效並行演算法，該演算法具有計數語義。
- MonPoly: LTL 的一階擴充套件，豐富了聚合模態。
- ARTiMon: 用於分析帶時間戳觀察流的工具，可用於檢測以基於時間邏輯的語言表達的危險。
跟蹤檢查分析的結果用於細化在設計時使用D-VerT驗證的應用程式模型。
跟蹤檢查在執行時執行，但它基於在設計時定義的帶註釋的 DTSM 模型，這些模型包含正在分析的拓撲。
DICE-TraCT 被設計為包含 Soloist 語言 Soloist，它提供以下類別的聚合模態
- 事件e在長度為d的時間視窗中的出現次數，
- 事件e的最大/平均出現次數，在長度為d的時間視窗中，對右對齊的相鄰非重疊子間隔（大小為h）進行聚合，
- 在長度為d的時間視窗中，發生在事件對e和e之間的平均時間，該事件對是特定相鄰且交替的事件。
但是，一些基本功能，例如在給定時間視窗中對事件進行平均，已在簡單的跟蹤分析器中開發，以提高工具的靈活性。因此，使用者可以利用最合適的引擎來執行日誌分析。
DICE-TraCT 具有客戶端-伺服器架構：客戶端元件是與 DICE IDE 完全整合的Eclipse 外掛，伺服器元件是 RESTful Web 伺服器。客戶端元件管理從使用者定義的 DTSM 模型到中間 JSON 物件的轉換，然後使用該物件呼叫伺服器。伺服器元件基於 JSON 檔案的內容為跟蹤檢查引擎生成跟蹤檢查例項。
DICE-TraCT 是一個 Eclipse 外掛，可以在 DICE IDE 中執行。要執行跟蹤檢查分析，必須使用 DICE::Storm 配置檔案透過 UML 類圖和活動圖來指定 Storm 拓撲。這些圖表可以透過拖放 DICE 工具欄中提供的 Eclipse 專案來輕鬆繪製，而註釋可以在 DICE IDE 的底部面板中指定。
DICE-TraCT 可以透過合適的執行配置視窗進行設定，允許使用者啟動分析。使用者可以指定
- 包含正在分析的模型的檔案，
- 限制分析時間視窗持續時間的時限，
- 將透過拓撲日誌計算其度量（sigma 和 avg_emit_rate）的Storm bolts 和 spouts 集，
- DICE-TraCT 伺服器正在執行的 IP 地址和埠，以及
- 監控平臺的 IP 地址和埠。
跟蹤檢查是在執行的部署應用程式上執行的，該應用程式是透過一個由**D-VerT**（驗證工具）驗證的抽象模型設計的，並且可能還使用了從模擬和最佳化工具獲得的結果。用**D-VerT**進行分析所使用的引數值與透過**DICE-TraCT**對應用程式日誌跟蹤進行分析所獲得的當前值進行比較。根據分析的型別（計數、平均值或定量）和拓撲結構，**DICE-TraCT**從監控平臺（D-Mon）中檢索日誌並執行分析。結果可用後，將顯示在DICE IDE中，以便使用者可以改進應用程式模型，重新執行驗證工具，並根據分析結果，根據需要更改實現。這個過程是迭代的，可以重複進行，直到驗證工具不再檢測到可能導致部署的應用程式在執行時出現意外行為的異常。
當日志包含合適的條目，能夠評估時間公式或指標時，應用程式日誌的跟蹤檢查可以成功實現。當要檢查的屬性僅引用由執行應用程式的資料密集型平臺的監控服務跟蹤的應用程式事件時，只需定義要評估的屬性（或指標）並在選定的日誌歷史記錄上執行跟蹤檢查器即可。另一方面，當要檢查的屬性引用應用程式框架未原生監控的應用程式事件時，跟蹤檢查需要對應用程式程式碼進行特定於應用程式的檢測，以便監控服務可以記錄評估感興趣屬性所需的那些特定於應用程式的事件。
**DICE-TraCT**目前支援Storm日誌分析。
**DICE-TraCT**的當前實現能夠分析兩個與**D-VerT**執行的驗證分析密切相關的不同引數。特別是，**DICE-TraCT**可以計算的兩個可用指標是
- *`avg_emit_rate`* 是一個Spout節點的傳送速率，定義為每秒傳送的元組數量，以及
- *`sigma`* 是Bolt節點輸出的元組數量與接收的元組數量之比。
透過跟蹤檢查獲得的指標值可以幫助設計人員調整用於驗證的模型，使用**D-VerT**。
跟蹤檢查分析可以僅限於特定的時間視窗，並且只考慮在有限時間內發生的日誌條目。大小決定了多少日誌事件被考慮用於評估指標（單位是毫秒）。
DICE-TraCT實現了三種不同的分析方式來計算指標。每種方式都依賴於用於分析日誌的基礎引擎的特性。參與跟蹤檢查分析的邏輯語言通常是指標時態邏輯的擴充套件，這些邏輯提供稱為聚合模態的特殊運算子。這些運算子對於在日誌中計數事件或計算特定時間視窗內發生次數的平均值並將該值與給定閾值進行比較很有用。因此，分析結果始終是布林答案，可以是“是”或“否”。**DICE-TraCT**基於Soloist，但**DICE-TraCT**的當前實現也可以呼叫比Soloist更簡單的跟蹤檢查器，該檢查器旨在提供從日誌中計算出的定量資訊。
以下型別的分析可用
- *`counting`*：透過Soloist邏輯的所謂計數公式，它能夠評估選定的指標。此選項將呼叫Soloists跟蹤檢查器。
- *`average`*：透過Soloist邏輯的所謂平均公式，它能夠評估選定的指標。此選項將呼叫Soloists跟蹤檢查器。
- *`quantitative`*：它能夠對日誌進行定量分析，提取指標的值。
由Soloist跟蹤檢查器例項化的分析旨在提供布林結果，該結果透過將日誌中事件的發生次數與使用者定義的閾值進行比較來計算。當啟動**DICE-TraCT**時，關係<、=和>以及閾值可以透過適當的配置視窗指定。
**DICE-TraCT**是一個Eclipse外掛，可以在DICE IDE中執行。為了進行日誌分析，必須使用UML類圖和活動圖來指定Storm拓撲。可以使用DICE工具欄中可用的Eclipse專案透過拖放來輕鬆繪製圖表，而註釋可以在DICE IDE的底部面板中指定。
圖2描述了實現Wikistats拓撲的Storm拓撲（有關實現詳細資訊，請參閱GitHub儲存庫）。該圖是一個DTSM模型，它也用於**D-VerT**的分析。
**DICE-TraCT**可以透過“執行配置”視窗設定，允許使用者啟動分析。使用者可以指定
- 包含正在分析的模型的檔案，
- 正在分析的Storm元件，
- **DICE-TraCT**伺服器執行的IP地址和埠。
分析允許提取與驗證相關的模型引數，即在D-VerT分析的正式模型中使用的值。DICE-TraCT提取以下引數值
- sigma：Bolt傳送的元組數量與接收的元組數量之比。
- alpha：Bolt處理一個元組所需的平均時間。
- 傳送速率：Spout的平均傳送速率。
圖3顯示了**DICE-TraCT**的執行配置以及定義Wikistats拓撲的元件列表。此外，圖中右側的最後一列顯示了在執行**DICE-TraCT**後，拓撲中某些元件的分析結果。
**DICE-TraCT**旨在執行Storm應用程式的日誌分析。它用於評估已部署應用程式的執行時行為，因為它會分析從監控平臺收集的日誌跟蹤，以驗證其是否符合設計時假設的行為模型。如果執行時行為不符合設計，則必須改進設計，然後重新驗證以獲得新的正確性認證。跟蹤檢查可以應用於向D-VerT執行的驗證任務提供資訊。跟蹤檢查從真實執行中提取D-VerT使用的模型引數值，這些值無法從框架的監控服務中獲取，因為它們本質上是驗證採用的建模的特定值。