作者 |李建文華東師范大學(xué)軟件工程學(xué)院博導(dǎo)

版塊 |鑒源論壇 · 觀模

01模型檢查的歷史

模型檢查是一種起源于20世紀(jì)70年代末的形式化驗(yàn)證技術(shù)。該技術(shù)最初由Edmund M. Clarke、E. Allen Emerson和Joseph Sifakis提出，他們因在模型檢查領(lǐng)域的貢獻(xiàn)而獲得了2007年的圖靈獎(jiǎng)。模型檢查的提出最初是為了對(duì)并發(fā)和分布式系統(tǒng)做自動(dòng)化驗(yàn)證，這些系統(tǒng)越來(lái)越復(fù)雜，手動(dòng)驗(yàn)證則變得越來(lái)越困難。模型檢查涉及系統(tǒng)地探索系統(tǒng)的所有可能狀態(tài)，并檢查每個(gè)狀態(tài)是否滿(mǎn)足某些屬性。

在早期階段，模型檢查可以通過(guò)顯示地計(jì)算Kripke結(jié)構(gòu)上的不動(dòng)點(diǎn)(針對(duì)CTL描述的性質(zhì)) [1]或者是在由模型和LTL性質(zhì)構(gòu)造的乘積自動(dòng)機(jī)上做狀態(tài)搜索 [2]來(lái)完成。盡管這些技術(shù)非常直觀且易于理解，但它們處理大型系統(tǒng)的能力非常有限，現(xiàn)在它們已經(jīng)被以BDD [3]和SAT求解器 [4]為計(jì)算核心的符號(hào)模型檢查技術(shù)所取代。事實(shí)上，基于SAT求解器的模型檢查技術(shù)是目前最有前景的自動(dòng)化驗(yàn)證技術(shù)。目前最先進(jìn)的基于SAT求解器的模型檢查技術(shù)包括BMC [5]，IMC [6]，IC3/PDR [7]，和CAR [8]。

模型檢查已被應(yīng)用于各種系統(tǒng)，包括硬件電路、通信協(xié)議、操作系統(tǒng)和軟件程序。它已被用于在部署之前檢測(cè)系統(tǒng)中的錯(cuò)誤和缺陷，這可以在開(kāi)發(fā)過(guò)程中節(jié)省時(shí)間和金錢(qián)。今天，模型檢查是一個(gè)活躍的研究和開(kāi)發(fā)領(lǐng)域，研究人員正在不斷努力，以提高其拓展性、準(zhǔn)確性和可用性。

02模型檢查問(wèn)題描述

模型檢查問(wèn)題是說(shuō)：給定一個(gè)模型M，或者說(shuō)一個(gè)狀態(tài)遷移系統(tǒng)，如何判斷M是否滿(mǎn)足安全性質(zhì)P。在具體算法實(shí)現(xiàn)中，我們往往是從初始狀態(tài)I出發(fā)，判斷┐P代表的狀態(tài)是否可達(dá)，即是否所有I可達(dá)的狀態(tài)都是滿(mǎn)足安全性質(zhì)P的。如果我們?cè)谒惴ㄖ姓业搅朔蠢?，即從I出發(fā)，經(jīng)過(guò)一系列狀態(tài)，可以到達(dá)┐P，則我們返回反例，用以說(shuō)明安全性質(zhì)P不成立；如果我們找到了一個(gè)不變式，即證明了從I出發(fā)，所有可達(dá)的范圍都在一個(gè)滿(mǎn)足P的狀態(tài)集合中，則我們返回驗(yàn)證通過(guò)，安全性質(zhì)P成立。下面我們先簡(jiǎn)要介紹幾個(gè)常見(jiàn)的模型檢查算法。

圖1 模型檢查問(wèn)題示例圖

03模型檢查算法介紹

3.1 Bounded Model Checking (BMC)

BMC是一個(gè)簡(jiǎn)單但是高效的模型檢查算法，類(lèi)似于圖搜索中的廣度優(yōu)先搜索。BMC從初始狀態(tài)出發(fā)，先判斷是否可以直接一步轉(zhuǎn)移到┐P，也就是不安全的狀態(tài)中，若可以，則找出了一個(gè)長(zhǎng)度為1的反例；若不行，則說(shuō)明在初始狀態(tài)一步的范圍內(nèi)，安全性質(zhì)成立，接著，BMC增大步數(shù)，判定從初始狀態(tài)出發(fā)，是否可以?xún)刹睫D(zhuǎn)移到┐P，同樣地，若可達(dá)則返回反例，若不可達(dá)，則繼續(xù)增大步數(shù)，直到找到反例或者達(dá)到限定的時(shí)間為止。

如下圖所示，從S0出發(fā)，先確定一步可達(dá)的S1和S2滿(mǎn)足性質(zhì)，接著增大步數(shù)，確定兩步可達(dá)的S3滿(mǎn)足性質(zhì)，再確定三步可達(dá)的S4和S5滿(mǎn)足性質(zhì)，最終步數(shù)為4時(shí)，檢查出四步可達(dá)的S6不滿(mǎn)足性質(zhì)，從而得到反例。

使用BMC算法可以很快地找到長(zhǎng)度最短的反例，但是它的局限性也很大，假設(shè)BMC在k步之內(nèi)找不到反例，這只能說(shuō)明初始狀態(tài)k步可達(dá)的狀態(tài)滿(mǎn)足安全性質(zhì)，而不能證明初始狀態(tài)可達(dá)的狀態(tài)都是滿(mǎn)足安全性質(zhì)的，也就是說(shuō)，BMC只適用于反例的尋找，而不適合證明模型滿(mǎn)足安全性質(zhì)。

圖2：BMC算法示例圖

3.2 Interpolation Model Checking (IMC)

IMC是在BMC的基礎(chǔ)上改進(jìn)來(lái)的模型檢查算法，它不僅可以查找反例，也可以證明模型是滿(mǎn)足安全性質(zhì)P的，彌補(bǔ)了BMC算法的缺陷。

簡(jiǎn)要地說(shuō)，在查找反例上，IMC和BMC一樣，都是靠確定從初始狀態(tài)出發(fā)，┐P代表的非安全狀態(tài)是否是k步可達(dá)的，如果是，則找到了反例，若不是，則繼續(xù)增大k的值。和BMC不同的是，對(duì)于每一個(gè)步數(shù)k，IMC都維持了一個(gè)初始狀態(tài)k步之內(nèi)可達(dá)的狀態(tài)的超集R，即R里面也包含了一些其他的狀態(tài)，且R里面的元素都滿(mǎn)足安全性質(zhì)，在尋找反例的過(guò)程中，IMC不斷擴(kuò)大集合R，若在某個(gè)時(shí)刻，R不能被擴(kuò)大，即R里面的元素只能轉(zhuǎn)移到R里面，則我們找到了一個(gè)不變式，即證明了從初始狀態(tài)出發(fā)，可達(dá)的所有狀態(tài)都是滿(mǎn)足安全性質(zhì)的，從而證明了模型是滿(mǎn)足安全性質(zhì)P的。

如下圖所示，從初始狀態(tài)S0出發(fā)，我們找到了一個(gè)狀態(tài)集合R，使得S0可達(dá)的狀態(tài)S1、S2和S3都在集合R中，且R中的元素都滿(mǎn)足安全性質(zhì)，因此我們證明了模型是滿(mǎn)足安全性質(zhì)的，集合R就是證據(jù)。

圖3 IMC算法示例圖

3.3 Property Directed Reachability (PDR)

PDR是一個(gè)較為復(fù)雜的模型檢查算法，簡(jiǎn)要地說(shuō)，它維持了一個(gè)滿(mǎn)足安全性質(zhì)P的狀態(tài)集合的序列F，其中F(0)是初始狀態(tài)I，而F(1)則是初始狀態(tài)一步之內(nèi)可達(dá)的集合的超集，即它里面除了有初始狀態(tài)一步之內(nèi)可達(dá)的狀態(tài)，也包含了一些其他的狀態(tài)，以此類(lèi)推，后面每一個(gè)F(i)集合都是前一個(gè)F(i-1)集合的一步之內(nèi)可達(dá)的集合的超集，PDR算法不斷地在F(i)集合中尋找那些可以一步轉(zhuǎn)移到┐P的元素S，若F(i)中的其他元素可以一步轉(zhuǎn)移到S，則PDR接著判斷F(i-1)中的元素可不可以?xún)刹睫D(zhuǎn)移到S，以此類(lèi)推，若在F(0)，即初始狀態(tài)中，有元素可以多步轉(zhuǎn)移到S，則找到了一個(gè)反例，即性質(zhì)P不成立，如果在這個(gè)過(guò)程中，我們找到一個(gè)F(i)集合，使得它里面的元素都不能轉(zhuǎn)移到S，則我們可以把S從這個(gè)集合及它之前的集合中刪除，我們不斷重復(fù)這個(gè)過(guò)程，如果在某一步，存在某個(gè)F(i)使得F(i)=F(i-1)，即F(i-1)里面的狀態(tài)只能轉(zhuǎn)移到F(i-1)里面時(shí)，我們就找到了一個(gè)不變式，即所有初始狀態(tài)可達(dá)的狀態(tài)都滿(mǎn)足了性質(zhì)P，證明了性質(zhì)P成立。

如下圖所示，在集合F(i+1)中，狀態(tài)S4可以一步轉(zhuǎn)移到非安全狀態(tài)S6，但是集合F(i+1)中的其他集合不能轉(zhuǎn)移到S4，因此我們把S4從Fi+1及其之前的集合中刪除，刪除S4后，我們發(fā)現(xiàn)集合F(i+1)和F(i)相等，即此時(shí)F(i)里面的狀態(tài)只能轉(zhuǎn)移到F(i)里面，因?yàn)镕(i)是初始狀態(tài)可達(dá)的狀態(tài)的超集，從而初始狀態(tài)可達(dá)的元素都在F(i)中，因此模型的安全性質(zhì)就得到了滿(mǎn)足，F(xiàn)(i)就是證據(jù)。

圖4 PDR算法示例圖

3.4 Complementary Approximate Reachability (CAR)

CAR算法也是一個(gè)較為復(fù)雜的模型檢查算法，可以有兩個(gè)搜索方向（Forward CAR和Backward CAR），后續(xù)我們以Backward CAR為例。CAR維護(hù)了兩個(gè)序列，B序列和F序列，F(xiàn)序列是從初始狀態(tài)I出發(fā)可達(dá)的狀態(tài)的子集的集合，B序列則是可以到達(dá)非安全狀態(tài)的!P的狀態(tài)的超集的集合，且F(0)= I , B(0)= !P。維護(hù)子集與超集的原因是F序列和B序列都是動(dòng)態(tài)的，F(xiàn)i的元素會(huì)隨著算法運(yùn)行不斷增多，子集會(huì)越來(lái)越接近原集。而B(niǎo)(i)的元素則會(huì)不斷減少，超集也會(huì)越來(lái)越接近原集。CAR算法就是不斷地去做類(lèi)似的SAT調(diào)用，然后根據(jù)結(jié)果去更新F和B序列。例如CAR算法會(huì)不斷地通過(guò)SAT來(lái)判斷某個(gè)狀態(tài)s能否一步轉(zhuǎn)移到B(i)，若成立，則可以拿到s的一個(gè)后繼狀態(tài)s'并把其加入到F序列，隨后CAR則遞歸詢(xún)問(wèn)s'是否可以轉(zhuǎn)移到B(i-1)；若不成立，CAR則會(huì)拿到一個(gè)uc(最小不滿(mǎn)足核)，并把這個(gè)uc來(lái)更新B(i+1)。

若存在某個(gè)B(i)，其是所有B(j) (j < i) 的并集的子集，那么模型是安全的。安全性條件生效表明B序列不會(huì)再擴(kuò)大，即使繼續(xù)擴(kuò)展B序列，新的B(i+1)中的元素，只會(huì)是下標(biāo)更小的B(i)中出現(xiàn)過(guò)的元素，這意味著初始狀態(tài)I不可能到達(dá)B(0)，因此模型是安全的。此時(shí)從B0至B(i)的并集構(gòu)成了一個(gè)不變式。如果某一個(gè)狀態(tài)空間F(i)中，存在一個(gè)狀態(tài)s，此狀態(tài)屬于非安全狀態(tài)!P，則得到一條以I為起點(diǎn)，狀態(tài)s為終點(diǎn)路徑，這條路徑是待驗(yàn)證性質(zhì)的反例，將被返回。

如下圖所示，我們發(fā)現(xiàn)集合B(i+1)包含在所有B(j) (j < i+1) 的并集中，因此安全性條件生效，B(j) (j < i+1) 的并集就是我們要找的不變式(安全性證明)。

圖5 CAR算法示例圖

參考文獻(xiàn)：

[1] E. Clarke and H. Schlingloff, “Model checking,” in Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. MIT Press, 2001, pp. 1635–1790.

[2] O. Kupferman, N. Piterman, and M. Y. Vardi, “An automata-theoretic approach to infinite-state systems,” in Time for Verification: Essays in Memory of Amir Pnueli, Z. Manna and D. A. Peled, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 202–259.

[3] K. L. McMillan, Symbolic Model Checking. Boston, MA: Springer US, 1993.

[4] Y. Vizel, G. Weissenbacher, and S. Malik, “Boolean satisfiability solvers and their applications in model checking,” Proceedings of the IEEE, vol.103, no. 11, pp. 2021–2035, 2015.

[5] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, “Symbolic model checking without BDDs,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS), W. R. Cleaveland, Ed. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 193–207.

[6] K. L. McMillan, “Interpolation and SAT-based model checking,” in Computer Aided Verification, W. A. Hunt and F. Somenzi, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003, pp. 1–13.

[7] A. R. Bradley, “SAT-based model checking without unrolling,” in Verification, Model Checking, and Abstract Interpretation, R. Jhala and D. Schmidt, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 70–87.

[8] J. Li, R. Dureja, G. Pu, K. Y. Rozier, and M. Y. Vardi, “Simplecar: An efficient bug-finding tool based on approximate reachability,” in Computer Aided Verification, H. Chockler and G. Weissenbacher, Eds. Cham: Springer International Publishing, 2018, pp. 37–44.

審核編輯黃宇