摘要：近年來,基于Petri網(wǎng)可覆蓋性的驗證技術已經(jīng)成功地應用于并發(fā)程序的驗證與分析中。然而,由于Petri網(wǎng)的可覆蓋性問題復雜度太高,這類技術在應用時有較大的局限性,對于輸入規(guī)模較大的問題常常會出現(xiàn)超時的情況。而Petri網(wǎng)的一個子系統(tǒng)非交互式Petri網(wǎng),其可覆蓋性和可達性復雜性均是NP完備的,同時表達力又可以作為某類并發(fā)程序的驗證模型。設計并實現(xiàn)了可以高效驗證非交互式Petri網(wǎng)可覆蓋性的工具CFPCV。采用基于約束的方法,從模型中提取約束,并使用Z3 SMT求解器對約束進行求解,同時,通過子網(wǎng)可標記方法對候選解進行驗證,從而保證每組解都是正確解。通過實驗分析了該工具的成功率、迭代次數(shù)以及運行效率,發(fā)現(xiàn)該算法不僅驗證成功率高,而且性能非常優(yōu)異。