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