摘要：近年來(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)異。