[發明專利]基于PD-Net的并發系統檢錯方法、系統、介質及設備

有效

• 申請號: 201810280956.X
• 申請日: 2018-04-02
• 公開（公告）號: CN108647380B
• 公開（公告）日: 2020-07-14
• 發明（設計）人: 蔣昌俊;閆春鋼;劉關俊;張亞英;楊波;相東明
• 申請（專利權）人: 同濟大學
• 主分類號: G06F30/22
• 分類號: G06F30/22;G06N7/00
• 代理公司: 上海光華專利事務所(普通合伙) 31219
• 代理人: 王華英

一種基于PD?Net的并發系統檢錯方法、系統、介質及設備，包括：使用PD?Net構建并發系統的PD?Net模型；分析PD?Net模型，獲取變遷關系信息，計算變遷關系信息得變遷可達信息和變遷沖突信息，排除變遷沖突信息得變遷并發信息；以預設判斷條件篩選變遷并發信息定位錯誤概率不為零的可疑目標狀態集；使用啟發式方法生成可達圖，使用預設路徑選擇方法從初始狀態逼近目標狀態，根據可達圖中的目標逼近結果信息檢測并發系統的數據不一致錯誤，本發明解決了現有技術中存在的缺少并發系統檢錯方法、數據流錯誤檢測精度差、檢測效率低、狀態空間爆炸的技術問題。

技術領域

本發明涉及一種并發檢測方法，特別是涉及一種基于PD-Net的并發系統檢錯方法、系統、介質及設備。

背景技術

隨著計算機技術的飛速發展，并發系統在我們的生活中也越來越常見。并發系統中的數據錯誤問題，可能會導致資金受損、業務停滯等。因此在并發系統投入使用之前對其進行驗證有著十分重要的現實意義。Petri網作為一種有完備自動化理論的形式描述語言，可以描述系統中的順序、并發、沖突以及同步關系，還有直觀地圖形表達方式。這些特點使其被廣泛用于并發系統的建模與分析。PD-Net作為Petri-net的擴展，在其上添加數據以及對數據的操作，不僅具有Petri網良好的性質，還能較好地描述并發系統中數據的操作，更適合用于并發系統的建模。模型驗證技術被廣泛用于分析模型中存在的錯誤。對于控制流錯誤的分析驗證已較為成熟，而對于數據流錯誤的研究則相對較少。數據不一致錯誤往往是不當地對同一數據進行并發操作造成的。現有的技術大多基于可達圖或網的展開技術對錯誤進行分析。但是當并發系統規模較大、并發操作較多時，會導致可達圖狀態空間爆炸，檢測需要耗費大量的時間與空間。

綜上，現有技術存在并發系統檢錯相關研究較少、一致性錯誤精度低定位慢的特點，現有技術中存在的缺少并發系統檢錯方法、數據流錯誤檢測精度差、檢測效率低、狀態空間爆炸的技術問題。

發明內容

鑒于以上現有技術的缺點，本發明的目的在于提供一種基于PD-Net的并發系統檢錯方法、系統、介質及設備，為解決現有技術中存在的缺少并發系統檢錯方法、數據流錯誤檢測精度差、檢測效率低、狀態空間爆炸的技術問題，本發明提供基于PD-Net的并發系統檢錯方法、系統、介質及設備，一種基于PD-Net的并發系統檢錯方法，包括：使用PD-Net構建并發系統的PD-Net模型；分析PD-Net模型，獲取變遷關系信息，計算變遷關系信息得變遷可達信息和變遷沖突信息，排除變遷沖突信息得變遷并發信息；以預設判斷條件篩選變遷并發信息定位錯誤概率不為零的可疑目標狀態集；使用啟發式方法生成可達圖，使用預設路徑選擇方法從初始狀態逼近目標狀態，根據可達圖中的目標逼近結果信息檢測并發系統的數據不一致錯誤。

于本發明的一實施方式中，分析PD-Net模型，獲取變遷關系信息，計算變遷關系信息得變遷可達信息和變遷沖突信息，排除變遷沖突信息得變遷并發信息，包括：獲得模型的庫所- 變遷的關系矩陣P*T，其中P為庫所數量，T為變遷數量；根據庫所-變遷的關系矩陣P*T得到變遷沖突矩陣，變遷數量T得變遷關系矩陣T*T；根據Warshall算法變遷關系矩陣T*T，得到變遷可達矩陣；根據變遷關系矩陣P*T中的變遷不可達信息和變遷可達矩陣得變遷沖突矩陣；排除變遷關系矩陣P*T對應的變遷關系中變遷沖突矩陣對應的沖突關系得變遷并發關系集合。

于本發明的一實施方式中，以預設判斷條件篩選變遷并發信息定位錯誤概率不為零的可疑目標狀態集，包括：獲取變遷并發關系集合；循環判斷變遷并發關系集合中的并發變遷t0 和t1是否滿足條件：(Read(t0)∪Write(t0)∪Delete(t0))∩(Write(t1)∪Delete(t1))其中Read(t0)代表并發變遷t0的數據進行讀取操作，Write(t0)代表并發變遷t0的數據進行寫入操作，Delete(t0)代表并發變遷t0的數據進行刪除操作，Write(t1) 代表并發變遷t1的寫入操作，Delete(t1)代表并發變遷t1的刪除操作；若是，則將變遷存入可疑目標狀態集；若否，則將繼續判斷變遷并發關系集合中的其他變遷直至遍歷變遷并發關系集合。