非交互式Petri網(wǎng)可覆蓋性驗證的高效實現(xiàn)
作者：丁如江; 李國強 上海交通大學(xué)軟件學(xué)院; 上海200240
摘要：近年來,基于Petri網(wǎng)可覆蓋性的驗證技術(shù)已經(jīng)成功地應(yīng)用于并發(fā)程序的驗證與分析中。然而,由于Petri網(wǎng)的可覆蓋性問題復(fù)雜度太高,這類技術(shù)在應(yīng)用時有較大的局限性,對于輸入規(guī)模較大的問題常常會出現(xiàn)超時的情況。而Petri網(wǎng)的一個子系統(tǒng)非交互式Petri網(wǎng),其可覆蓋性和可達性復(fù)雜性均是NP完備的,同時表達力又可以作為某類并發(fā)程序的驗證模型。設(shè)計并實現(xiàn)了可以高效驗證非交互式Petri網(wǎng)可覆蓋性的工具CFPCV。采用基于約束的方法,從模型中提取約束,并使用Z3 SMT求解器對約束進行求解,同時,通過子網(wǎng)可標記方法對候選解進行驗證,從而保證每組解都是正確解。通過實驗分析了該工具的成功率、迭代次數(shù)以及運行效率,發(fā)現(xiàn)該算法不僅驗證成功率高,而且性能非常優(yōu)異。
注：因版權(quán)方要求，不能公開全文，如需全文，請咨詢雜志社。
軟件學(xué)報雜志
軟件學(xué)報雜志， 月刊，本刊重視學(xué)術(shù)導(dǎo)向，堅持科學(xué)性、學(xué)術(shù)性、先進性、創(chuàng)新性，刊載內(nèi)容涉及的欄目：理論計算機科學(xué)、系統(tǒng)軟件與軟件工程、模式識別與人工智能、數(shù)據(jù)庫技術(shù)、計算機網(wǎng)絡(luò)與信息安全、計算機體系結(jié)構(gòu)等。于1990年經(jīng)新聞總署批準的正規(guī)刊物。
- 北大期刊
- CSCD期刊
- 統(tǒng)計源期刊
- 1-3個月審核
