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