基于分布式系統(tǒng)的軟件模型驗證加速方法研究.pdf

1、模型驗證方法在軟件可靠性檢測方面性能卓越，但數(shù)據(jù)結(jié)構(gòu)復(fù)雜的軟件系統(tǒng)會引起狀態(tài)空間爆炸問題。分布式系統(tǒng)可加速驗證速率，但其不穩(wěn)定性會導(dǎo)致模型驗證效率低下甚至驗證失敗結(jié)果。研究如何提取軟件系統(tǒng)驗證有效部分，解決如何將模型驗證移植到分布式系統(tǒng)處理等問題，對提升驗證效率及擴(kuò)展代碼規(guī)模具有非凡的研究意義與應(yīng)用價值。
　　本文將對程序本身處理的前端和分布式加速計算的后端相結(jié)合，在前端處理中，通過根據(jù)驗證性質(zhì)對源程序切片，循環(huán)執(zhí)行路徑壓縮等方法

2、簡化標(biāo)準(zhǔn)C源程序，從而提取程序主干框架。進(jìn)而在此基礎(chǔ)上通過狀態(tài)劃分，生成更簡單高效的CTL自動機(jī)模型，提高驗證性質(zhì)的定位能力。然后進(jìn)入后端處理，通過重新設(shè)計CTL狀態(tài)自動機(jī)的數(shù)據(jù)結(jié)構(gòu)，以及改進(jìn)模型驗證標(biāo)記算法，從而使軟件模型驗證問題適用于分布式系統(tǒng)Hadoop架構(gòu)中的MapReduce框架。在分布式加速計算后，可輸出滿足驗證性質(zhì)的軟件模型狀態(tài)集合，進(jìn)而獲取驗證結(jié)果。同時，針對分布式系統(tǒng)運(yùn)行節(jié)點易失效降低驗證效率的問題，編寫分布式系統(tǒng)中Z