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

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

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