[發(fā)明專利]基于TLA+形式化規(guī)范模型檢查的分布式系統(tǒng)測試方法及裝置

在審

• 申請?zhí)枺?/td>: 202211041081.0
• 申請日: 2022-08-29
• 公開（公告）號: CN115309654A
• 公開（公告）日: 2022-11-08
• 發(fā)明（設計）人: 竇文生;王棟;高鈺;吳陳傲;魏峻;黃濤
• 申請（專利權(quán)）人: 中國科學院軟件研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京君尚知識產(chǎn)權(quán)代理有限公司 11200
• 代理人: 陳艷

1.一種基于TLA+形式化規(guī)范模型檢查的分布式系統(tǒng)測試方法，其步驟包括：

針對目標分布式系統(tǒng)的TLA+形式化規(guī)范，將所述TLA+形式化規(guī)范的要素映射到所述目標分布式系統(tǒng)的實現(xiàn)中，并收集所述目標分布式系統(tǒng)的運行數(shù)據(jù)；其中，所述運行數(shù)據(jù)包括：運行時的節(jié)點狀態(tài)變量值和運行時的行為發(fā)生情況；

使用TLC模型檢查器驗證所述TLA+形式化規(guī)范，獲取驗證過正確性的抽象狀態(tài)空間圖；

對所述抽象狀態(tài)空間圖進行路徑遍歷，將得到的每一條路徑視為一個測試用例；

基于所述測試用例對所述目標分布式系統(tǒng)進行受控測試，得到受控測試數(shù)據(jù)；其中，所述受控測試數(shù)據(jù)包括：測試路徑中狀態(tài)節(jié)點的變量值和測試路徑中行為的發(fā)生情況；

將所述運行數(shù)據(jù)與所述受控測試數(shù)據(jù)進行比對，以生成測試報告。

2.如權(quán)利要求1所述的方法，其特征在于，所述要素包括：用作描述所述分布式系統(tǒng)內(nèi)狀態(tài)的變量要素和導致所述分布式系統(tǒng)內(nèi)狀態(tài)更新的行為要素，所述變量要素包括：狀態(tài)相關變量和消息相關變量，所述行為要素包括：節(jié)點內(nèi)部行為、消息相關行為、用戶請求和故障；所述故障包括：節(jié)點宕機、節(jié)點重啟、消息丟失和消息重復；其中，所述狀態(tài)相關變量用于定義分布式系統(tǒng)中的關鍵狀態(tài)值，所述消息相關變量用于以共享變量的形式模擬所述目標分布式系統(tǒng)消息通訊中的信息交流，所述節(jié)點內(nèi)部行為用于描述更新節(jié)點狀態(tài)值的行為，所述消息相關行為用于描述通過消息傳遞更新節(jié)點狀態(tài)值的行為，所述用戶請求用于描述由用戶發(fā)起的系統(tǒng)外部行為，所述故障用于描述外部不確定性行為。

3.如權(quán)利要求2所述的方法，其特征在于，所述將狀態(tài)相關變量映射到所述目標分布式系統(tǒng)的實現(xiàn)中，包括：

使用@Variable($VNAME$)標注所述狀態(tài)相關變量；其中，$VNAME$表示所述狀態(tài)相關變量在TLA+形式化規(guī)范中的命名；

針對每一所述狀態(tài)相關變量，基于所述狀態(tài)相關變量的標注在所述目標分布式系統(tǒng)中插樁，并為映射的變量加入一個靜態(tài)影子字段；其中，所述靜態(tài)影子字段用于基于所述節(jié)點狀態(tài)變量值被初始化或更新進行賦值。

4.如權(quán)利要求2所述的方法，其特征在于，所述將節(jié)點內(nèi)部行為映射到所述目標分布式系統(tǒng)的實現(xiàn)中，包括：

使用@Behavior($BNAME$)標注所述節(jié)點內(nèi)部行為；其中，所述$BNAME$表示所述節(jié)點內(nèi)部行為在TLA+形式化規(guī)范中的命名；

針對每一所述節(jié)點內(nèi)部行為，基于所述節(jié)點內(nèi)部行為的標注在所述目標分布式系統(tǒng)中插樁，并在每一個映射的行為方法的進入處及返回處插入一行代碼；其中，所述進入處的代碼用于收集行為參數(shù)的實時值，以阻塞方法繼續(xù)運行并等待返回的調(diào)度指令，所述返回處的代碼用于收集所有狀態(tài)相關變量的實時值。

5.如權(quán)利要求2所述的方法，其特征在于，所述將消息相關行為映射到所述目標分布式系統(tǒng)的實現(xiàn)中，包括：

標注所述消息相關行為；

針對每一所述節(jié)點內(nèi)部行為，基于所述消息相關行為的標注在所述目標分布式系統(tǒng)中插樁，以收集所述目標分布式系統(tǒng)中傳遞的消息值。

6.如權(quán)利要求2所述的方法，其特征在于，所述將用戶請求映射到所述目標分布式系統(tǒng)的實現(xiàn)中，包括：

利用所述目標分布式系統(tǒng)的用戶腳本，建立所述TLA+形式化規(guī)范中用戶請求行為與所述用戶腳本的對應關系；

基于所述對應關系，對所述用戶請求與所述用戶腳本進行匹配。

7.如權(quán)利要求2所述的方法，其特征在于，所述將故障映射到所述目標分布式系統(tǒng)的實現(xiàn)中，包括：

在所述故障為所述節(jié)點宕機或所述節(jié)點重啟的情況下，殺死該節(jié)點對應的進程并通過保存的節(jié)點配置進行重啟；

在所述故障為消息丟失故障的情況下，對消息及網(wǎng)絡相關代碼進行插樁，并忽略消息處理函數(shù)的內(nèi)部邏輯并直接返回；

在所述故障為消息重復故障的情況下，對消息及網(wǎng)絡相關代碼進行插樁，并在消息處理函數(shù)中對同一消息進行多次重復處理。