基於學習的快取一致性協議帶參驗證
一、背景
帶參系統存在於許多應用領域中，比如快取一致協議等。因為它的研究價值，驗證這樣的系統的也就吸引來了形式化驗證、模型檢測和定理證明等社群的關注。要想驗證帶參系統的正確性，就必須驗證任意例項大小的系統中的正確性，而這被證明是一個無法判定的問題。
儘管這樣的難度，但是很多方法仍然被提出來試圖解決這個問題。CMP方法是其中最成功的方法之一。它用模型檢測的方法來驗證Intel、flash等大型的協議。通過保留m個節點， 並用一個抽象的節點N Other 來替代其他所有剩餘節點的行為。通過這樣的抽象，一個原始的協議就被抽象成了一個由m+1個節點組成的抽象寫意。然後通過分析模型檢測器提供的反例，迴圈構造一系列引理來限制抽象節點N Other 的行為，使得協議可以收斂，且不會違反原有性質。如果最終原始性質和引理都能在抽象協議中被檢驗通過，那麼就能推匯出原始協議在任意大小的例項下也都能成立。但是，CMP方法是在模型檢測機給出反例之後，採取的是被動補救措施。這樣的被動方法由於依賴於人工理解和指導，而無法自動化。而且“尋找反例-衛式加強”這樣的迴圈，所需要的次數未知，這也就使得可達集是否能收斂、抽象協議能否滿足安全性質成為未知。
CMP存在的缺點啟發我們去更深入地思考：是否能夠通過主動地探索滿足上述條件的可達集邊緣，以使可達集收斂，並滿足安全性質？如果能夠主動的限定可達集能到達的範圍，則可以更主動地搜尋輔助不變式，從而更精確地加強抽象系統。
因此，在這篇論文中，我們提出了L-CMP，一種自動的學習框架，通過較小例項可達集學習/挖掘輔助不變式，並且自動的用這些輔助不變式對抽象協議進行限制，最終，抽象協議的可達集可以被收斂在合理範圍，安全性質也就能夠保證。
二、關聯規則學習
在本文中，我們巧妙地將關聯規則學習（Association rule learning）與衛式加強做結合，成功達到了尋找輔助不變式及自動衛式加強的目的。
關聯規則學習是Agrawal等人提出的基於規則的機器學習方法。它的目的是利用一些有趣性的量度來識別資料庫中發現的強規則。基於強規則的概念，Rakesh Agrawal等人引入了關聯規則以發現由超市的POS系統記錄的大批交易資料中產品之間的規律性。許多有效的關聯規則演算法，如Apriori，Eclat和FP-growth。在本文中，我們使用Apriori作為關聯規則的學習演算法進行學習。
給定由一組事務組成的資料集D，記為D = {t1，t2，…，tm}。 設I = {i1，i2，…，in}是一組包含許多專案的項集。 每個交易t包含一個專案子集。 一個關聯規則的形式是X→Y，其中X，Y∈ I. X被稱為前件，Y是規則的後件。 此外，還有一些約束條件來衡量規則的重要性。 在本文中，我們重點關注兩個標準：支援度和置信度。
支援度： 它測量在同一事務中發生的專案集的頻率。 K頻繁專案集是頻繁集合中包含K個專案的專案集。 可以將支援計算為在同一事務中出現多個專案的概率。 支援價值的最低閾值被稱為最小支援度。
三、框架
L-CMP可以分為以下兩個階段：
學習不變式：這個階段旨在通過學習演算法尋找出輔助不變數。在這個階段，我們首先收集協議的一個小例項 m（通常是m = 2）的可達狀態集合（步驟1）。然後，我們直接從協議描述中提取原子謂詞，並將它們看作專案集以指導資料集的轉換（步驟2）。這一步對於第二階段是必要的，第四節解釋了背後的原因。接下來，通過關聯規則學習，可以學習一組關聯規則（步驟3）。值得注意的是，我們使用的資料集由一個小型的協議例項進行轉換，因此由於例項的大小有限，無法表示整個引數化協議的行為。此外，我們已經應用了對稱減少技術來使一些大協議中的可達狀態最小化，導致資料集的不完整性。因此，需要額外的步驟（步驟4）。我們將這些關聯規則視為候選不變數並將它們輸入模型檢查器Murphi。如果他們持有協議的一些小例項（大於m），則它們被視為輔助不變數。如果某些失敗，失敗的將從候選不變集中消除。最後，左邊的候選不變數作為輔助不變數。
引數抽象和衛式加強： 這個階段是抽象協議，並使用輔助不變數加強抽象規則的衛式部分。首先，輔助不變數以及協議中的轉換規則將通過分配具體索引來例項化（步驟5）。這一步為加強步驟提供了便利。接下來，通過以關聯規則的形式新增輔助不變數的結果，遞迴地加強規則守護（步驟6）。然後，通過刪除關於不可觀察節點的區域性變數來抽象加強的規則（步驟7）。值得注意的是，我們提出了一個對映操作，它建立了守衛與行動之間的關係，以便最大限度地加強規則。之後，加強和抽象的規則將附加到原始協議並送入模型檢查器（步驟8）。請注意，用於加強守則規則的輔助不變數也需要驗證將它們翻譯成Murphi程式碼後。自動翻譯的過程較為簡單，所以我們在本文中就不贅述。如果抽象協議例項通過大小為$m + 1$的模型檢測器，則結束框架（步驟10），否則就需要調整學習演算法中的引數，並且框架開始下一輪學習（步驟9） 。
三、實驗結果
我們將L-CMP應用於5個經典的帶參協議上進行實驗，實驗結果如下表：
其中，列名分別為協議名稱、頻繁集個數、最小支援度、關聯規則個數、輔助不變式個數、所用不變式個數、總執行時長、所耗記憶體峰值、抽象協議能否通過驗證。
可以看到，我們的L-CMP能夠很好地對包括Flash協議在內的各個協議進行很好的驗證。
四、總結
在本文中，我們提出了一個自動框架L-CMP，它可以在一個統一的框架中自動學習輔助不變數，並進行抽象引數和衛式加強。 我們工作的創新性集中體現在於以下兩個方面：
我們不是通過分析計數器例子來手動制定不同的變體，而是通過關聯規則學習從協議的可達狀態集合中匯出不變數；
在反例生成之後，我們不再強化協議，而是根據自動學習的不變數直接進行衛式加強。
在未來的工作中，我們希望擴充套件L-CMP的驗證能力，使其能證明一般的安全性質和活性性質，而不僅侷限於不變式。
參考文獻
[1] Lv, Y., Lin, H., Pan, H.: Computing invariants for parameter abstraction.In: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign , IEEE Computer Society (2007) 29–38
[2] Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-stateconcurrent systems. Information Processing Letters 22(6) (1986) 307–309
[3] Chou, C.T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: FMCAD . Volume 4., Springer (2004) 382–398
[4] Agrawal,R.,Imielin ́ski,T.,Swami,A.:Miningassociationrulesbetweensets of items in large databases. In: Acm sigmod record . Volume 22.,ACM (1993) 207–216