SPIN狀態(tài)壓縮：基于屬性的狀態(tài)向量優(yōu)化.pdf

1、模型檢測是保證程序正確性的一條重要途徑，它最大的優(yōu)點(diǎn)就是驗證過程完全自動化。然而，模型檢測在規(guī)模大、復(fù)雜度高的系統(tǒng)的應(yīng)用中卻碰到了所謂狀態(tài)空間爆炸問題——對很多系統(tǒng)來說，其運(yùn)行過程中所產(chǎn)生的系統(tǒng)狀態(tài)數(shù)目往往隨著系統(tǒng)規(guī)模的擴(kuò)大和及其子模塊數(shù)目的增加而呈現(xiàn)指數(shù)增長。這直接導(dǎo)致很多系統(tǒng)的規(guī)模超出了當(dāng)前驗證工具的能力范圍。 SPIN是貝爾實(shí)驗室開發(fā)的面向分布式軟件系統(tǒng)的模型檢測器。SPIN在應(yīng)用過程中同樣面臨狀態(tài)空間爆炸問題，它采用偏序

2、歸約策略來減少狀態(tài)空間中需要遍歷及存儲的狀態(tài)數(shù)目。還有另一種完全不同的策略是減少每個系統(tǒng)狀態(tài)所需的存儲空間，這屬于內(nèi)存壓縮技術(shù)的范疇。 本文提出了一種基于SPIN的無損壓縮技術(shù)——基于屬性的狀態(tài)向量優(yōu)化(SOBP)，它利用系統(tǒng)屬性的特點(diǎn)，以一個變量替換多個變量的方式對狀態(tài)向量進(jìn)行優(yōu)化，從而實(shí)現(xiàn)狀態(tài)壓縮。而且，當(dāng)該算法與collapsecompression結(jié)合使用時，將使collapsecompression更加強(qiáng)大，從而進(jìn)一步