[發(fā)明專利]一種基于Event-B的多核并發(fā)系統(tǒng)驗證方法

有效

• 申請?zhí)枺?/td>: 201810067441.1
• 申請日: 2018-01-24
• 公開（公告）號: CN108228410B
• 公開（公告）日: 2020-09-25
• 發(fā)明（設計）人: 趙永望;郭煒鋒;張峰;譚宇
• 申請（專利權(quán)）人: 北京航空航天大學
• 主分類號: G06F11/28
• 分類號: G06F11/28
• 代理公司: 北京中創(chuàng)陽光知識產(chǎn)權(quán)代理有限責任公司 11003
• 代理人: 尹振啟

1.一種基于Event-B的多核并發(fā)系統(tǒng)驗證方法，其特征在于，包括：

步驟1，根據(jù)程序的原子性定義，分析多核系統(tǒng)服務需求，將完整的非原子服務需求劃分成多個原子需求；

步驟2，找出原子需求中核心的需求，進行抽象建模；

步驟3，通過抽象模塊進行求精，精化核心原子需求的同時，不斷加入其他新的原子需求，構(gòu)建服務需求精化模型；

步驟4，多個原子需求根據(jù)在服務需求中的描述順序，依次組合成完整的服務需求，構(gòu)建完整的服務需求模型；

步驟5，根據(jù)預設的專用公理集，對服務需求模型構(gòu)造不變式；

步驟6，根據(jù)不變式驗證原子需求是否滿足不變式的一致性；

步驟7，通過檢查原子需求是否滿足不變式的一致性，判斷服務需求存在的問題；所述原子需求包括自定義原子需求和服務原子需求；若所述原子需求為自定義原子需求，則所述原子需求組合成完整的服務需求，包括：基于所述服務需求的初始化原子需求組成所述服務需求的開始部分，基于所述服務需求的結(jié)束原子需求組成所述服務需求的結(jié)束部分；若所述原子需求為服務原子需求，則所述原子需求為服務需求所劃分的服務需求部分；

所述建模為將并發(fā)隊列模型劃分為2層；第一層模型，其描述并發(fā)隊列的入隊列操作和出隊列操作，入隊列和出隊列操作都采用鎖機制，轉(zhuǎn)換成抽象模型的enqueue和dequeue事件； 所述enqueue事件正常執(zhí)行的條件為新入的節(jié)點是未使用過的數(shù)值，隊列長度不超過最大長度；dequeue事件正常執(zhí)行的條件是確保出隊列的節(jié)點為已經(jīng)存在的節(jié)點，隊列不為空；第二層模型，其引入了多核模型將并發(fā)隊列具體化，入隊列和出隊列操作分解為相應的Event-B事件，然后進行建模，將抽象模型中的隊列操作精化成完整的并發(fā)隊列操作；

所述入隊列操作分為6個所述Event-B事件，所述6個Event-B事件包括初始化事件，滿隊列判斷事件，精化事件，喚醒事件，不喚醒事件，重置事件。

2.根據(jù)權(quán)利要求1所述的方法，其特征在于，所述構(gòu)建服務需求精化模型為精化原子需求和新添原子需求；若所述原子需求為精化原子需求，所述原子需求滿足所述抽象模型的原子需求；若所述原子需求為新添原子需求，所述原子需求滿足所述服務需求的原子需求。

3.根據(jù)權(quán)利要求1所述的方法，其特征在于，所述不變式包括服務需求模型不變式和服務需求安全性不變式；若所述不變式為服務需求模型不變式，則基于自動定理證明器、SMT求解器，驗證所述服務需求模型是否存在正確性問題；若所述不變式為服務需求安全性不變式，則基于自動定理證明器、SMT求解器驗證所述服務需求安全性是否存在安全性問題。

4.根據(jù)權(quán)利要求1所述的方法，其特征在于，還包括：當確定所述服務需求存在安全性問題之后，查找并記錄錯誤問題。