非交互式Petri网可覆盖性验证的高效实现
|
摘要
近年来,基于Petri网可覆盖性的验证技术已经成功地应用于并发程序的验证与分析中.然而,由于Petri网的可覆盖性问题复杂度太高,这类技术在应用时有较大的局限性,对于输入规模较大的问题常常会出现超时的情况.而Petri网的一个子系统——非交互式Petri网,其可覆盖性和可达性复杂性均是NP完备的,同时表达力又可以作为某类并发程序的验证模型.设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV.采用基于约束的方法,从模型中提取约束,并使用Z3SMT求解器对约束进行求解,同时,通过子网可标记方法对候选解进行验证,从而保证每组解都是正确解.通过实验分析了该工具的成功率、迭代次数以及运行效率,发现该算法不仅验证成功率高,而且性能非常优异.
In recent years, the verification technology based on Petri net coverability has been successfully applied to the verification and analysis of concurrent programs. However, due to the complexity of Petri net coverability, such technology has great limitations in application. For large scale input model, they all have timeout problem. While a subsystem of Petri net—communication-free Petri net,whose reachability and coverability are both NP-complete, can be used as a verification model of certain class of concurrent program because of its expression. In this study, a tool called CFPCV is designed and implemented, which can verify coverability of communication-free Petri net very efficiently. A constraint-based approach is used to extract the constraints from the model and solve the constraints with Z3 SMT solver, and then the candidate solutions are verified with subnet markable method to ensure that each solution is correct. The success rate, iteration times, and performance of the tool are experimentally analyzed, and it is found that the proposed algorithm has not only a high success rate but also excellent performance.
In recent years, the verification technology based on Petri net coverability has been successfully applied to the verification and analysis of concurrent programs. However, due to the complexity of Petri net coverability, such technology has great limitations in application. For large scale input model, they all have timeout problem. While a subsystem of Petri net—communication-free Petri net,whose reachability and coverability are both NP-complete, can be used as a verification model of certain class of concurrent program because of its expression. In this study, a tool called CFPCV is designed and implemented, which can verify coverability of communication-free Petri net very efficiently. A constraint-based approach is used to extract the constraints from the model and solve the constraints with Z3 SMT solver, and then the candidate solutions are verified with subnet markable method to ensure that each solution is correct. The success rate, iteration times, and performance of the tool are experimentally analyzed, and it is found that the proposed algorithm has not only a high success rate but also excellent performance.
引文
[1]BouajjaniA,EmmiM.Boundedphaseanalysisofmessage-passingprograms.Int’lJournalonSoftwareToolsforTechnology Transfer(STTT), 2014,16(2):127–146.
[2]D’OsualdoE,KochemsJ,OngCHL.Automaticverificationoferlang-styleconcurrency.In:Proc.oftheInt’lStaticAnalysis Symposium. Berlin:Springer-Verlag, 2013. 454–476.
[3]Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Trans. on Programming Languages and Systems,2012,34(1):1–48.
[4]Kaiser A, Kroening D, Wahl T. Efficient coverability analysis by proof minimization. In:Proc. of the Int’l Conf. on Concurrency Theory. Berlin:Springer-Verlag, 2012. 500–515.
[5]German SM, Sistla AP. Reasoning about systems with many processes. Journal of the ACM(JACM), 1992,39(3):675–735.
[6]KloosJ,MajumdarR,NiksicF,etal.Incremental,inductivecoverability.In:Proc.oftheInt’lConf.onComputerAided Verification. Berlin:Springer-Verlag, 2013. 158–173.
[7]Esparza J, Ledesma-Garza R, Majumdar R, et al. An SMT-based approach to coverability analysis. In:Proc. of the Int’l Conf. on Computer Aided Verification. Cham:Springer-Verlag, 2014. 603–619.
[8]EsparzaJ.Petrinets,commutativecontext-freegrammars,andbasicparallelprocesses.FundamentaInformaticae,1997,31(1):13–25.
[9]BarrettC,TinelliC.Satisfiabilitymodulotheories.JournalonSatisfiabilityBooleanModelingandComputation,2018,3(3):141–224.
[10]BofillM,NieuwenhuisR,OliverasA,etal.ThebarcelogicSMTsolver.In:Proc.oftheInt’lConf.onComputerAided Verification. Berlin:Springer-Verlag, 2008. 294–298.
[11]Jha S, Limaye R, Seshia SA. Beaver:Engineering an efficient SMT solver for bit-vector arithmetic. In:Proc. of the Int’l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2009. 668–674.
[12]Dutertre B, De Moura L. The YICES SMT solver. 2006. http://yices.csl.sri.com/tool-paper.pdf
[13]Moura LD, Bj?rner N. Z3:An efficient SMT solver. In:Proc. of the Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2008. 337–340.
[14]Delzanno G, Raskin JF, Begin LV. Towards the automated verification of multithreaded Java programs. In:Proc. of the Int’l Conf.on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2002. 173–187.
[15]GantyP,RaskinJF,BeginLV.Frommanyplacestofew:AutomaticabstractionrefinementforPetrinets.Fundamenta Informaticae, 2008,88(3):275–305.
[16]Geeraerts G, Raskin JF, Van Begin L. Expand, enlarge, and check:New algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 2006,72(1):180–203.
[17]Karp RM, Miller RE. Parallel program schemata. Journal of Computer and System Sciences, 1969,3(2):147–195.
[18]RackoffC.Thecoveringandboundednessproblemsforvectoradditionsystems.TheoreticalComputerScience,1978,6(2):223–231.
[19]Berthomieu B, Ribet PO, Vernadat F. The tool TINA—Construction of abstract state spaces for Petri nets and time Petri nets. Int’l Journal of Production Research, 2004,42(14):2741–2756.
[20]Geeraerts G, Raskin JF, Begin LV. On the efficient computation of the minimal coverability set for Petri net. In:Proc. of the Int’l Symp. on Automated Technology for Verification and Analysis. Berlin:Springer-Verlag, 2007. 98–113.
[21]Finkel A. Reduction and covering of infinite reachability trees. Information and Computation, 1990,89(2):144–179.
[22]Grahlmann B. The PEP tool. In:Proc. of the Int’l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 1997. 440–443.
[23]AbdullaPA,CeransK,JonssonB,etal.Generaldecidabilitytheoremsforinfinite-statesystems.In:Proc.oftheLogicin Computer Science(LICS’96). IEEE, 1996. 313–321.
[24]Meyer R, Strazny T. Petruchio:From dynamic networks to nets. In:Proc. of the Int’l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2010. 175–179.
[25]Finkel A. Monotonic extensions of Petri nets. Electronic Notes in Theoretical Computer Science, 2003,68(6):85–106.
[26]Ganty P, Raskin JF, Begin LV. A complete abstract interpretation framework for coverability properties of WSTS. In:Proc. of the Int’l Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin:Springer-Verlag, 2006. 49–64.
[27]GerthR,PeledD,VardiMY,etal.Simpleon-the-flyautomaticverificationoflineartemporallogic.In:ProtocolSpecification,Testing and Verification. Boston:Springer-Verlag, 1995. 3–18.
[28]Esparza J. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 1997,34(2):85–107.
[29]Murata T. Petri nets:Properties, analysis and applications. Proc. of the IEEE, 1989,77(4):541–580.
[2]D’OsualdoE,KochemsJ,OngCHL.Automaticverificationoferlang-styleconcurrency.In:Proc.oftheInt’lStaticAnalysis Symposium. Berlin:Springer-Verlag, 2013. 454–476.
[3]Ganty P, Majumdar R. Algorithmic verification of asynchronous programs. ACM Trans. on Programming Languages and Systems,2012,34(1):1–48.
[4]Kaiser A, Kroening D, Wahl T. Efficient coverability analysis by proof minimization. In:Proc. of the Int’l Conf. on Concurrency Theory. Berlin:Springer-Verlag, 2012. 500–515.
[5]German SM, Sistla AP. Reasoning about systems with many processes. Journal of the ACM(JACM), 1992,39(3):675–735.
[6]KloosJ,MajumdarR,NiksicF,etal.Incremental,inductivecoverability.In:Proc.oftheInt’lConf.onComputerAided Verification. Berlin:Springer-Verlag, 2013. 158–173.
[7]Esparza J, Ledesma-Garza R, Majumdar R, et al. An SMT-based approach to coverability analysis. In:Proc. of the Int’l Conf. on Computer Aided Verification. Cham:Springer-Verlag, 2014. 603–619.
[8]EsparzaJ.Petrinets,commutativecontext-freegrammars,andbasicparallelprocesses.FundamentaInformaticae,1997,31(1):13–25.
[9]BarrettC,TinelliC.Satisfiabilitymodulotheories.JournalonSatisfiabilityBooleanModelingandComputation,2018,3(3):141–224.
[10]BofillM,NieuwenhuisR,OliverasA,etal.ThebarcelogicSMTsolver.In:Proc.oftheInt’lConf.onComputerAided Verification. Berlin:Springer-Verlag, 2008. 294–298.
[11]Jha S, Limaye R, Seshia SA. Beaver:Engineering an efficient SMT solver for bit-vector arithmetic. In:Proc. of the Int’l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2009. 668–674.
[12]Dutertre B, De Moura L. The YICES SMT solver. 2006. http://yices.csl.sri.com/tool-paper.pdf
[13]Moura LD, Bj?rner N. Z3:An efficient SMT solver. In:Proc. of the Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2008. 337–340.
[14]Delzanno G, Raskin JF, Begin LV. Towards the automated verification of multithreaded Java programs. In:Proc. of the Int’l Conf.on Tools and Algorithms for the Construction and Analysis of Systems. Berlin:Springer-Verlag, 2002. 173–187.
[15]GantyP,RaskinJF,BeginLV.Frommanyplacestofew:AutomaticabstractionrefinementforPetrinets.Fundamenta Informaticae, 2008,88(3):275–305.
[16]Geeraerts G, Raskin JF, Van Begin L. Expand, enlarge, and check:New algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 2006,72(1):180–203.
[17]Karp RM, Miller RE. Parallel program schemata. Journal of Computer and System Sciences, 1969,3(2):147–195.
[18]RackoffC.Thecoveringandboundednessproblemsforvectoradditionsystems.TheoreticalComputerScience,1978,6(2):223–231.
[19]Berthomieu B, Ribet PO, Vernadat F. The tool TINA—Construction of abstract state spaces for Petri nets and time Petri nets. Int’l Journal of Production Research, 2004,42(14):2741–2756.
[20]Geeraerts G, Raskin JF, Begin LV. On the efficient computation of the minimal coverability set for Petri net. In:Proc. of the Int’l Symp. on Automated Technology for Verification and Analysis. Berlin:Springer-Verlag, 2007. 98–113.
[21]Finkel A. Reduction and covering of infinite reachability trees. Information and Computation, 1990,89(2):144–179.
[22]Grahlmann B. The PEP tool. In:Proc. of the Int’l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 1997. 440–443.
[23]AbdullaPA,CeransK,JonssonB,etal.Generaldecidabilitytheoremsforinfinite-statesystems.In:Proc.oftheLogicin Computer Science(LICS’96). IEEE, 1996. 313–321.
[24]Meyer R, Strazny T. Petruchio:From dynamic networks to nets. In:Proc. of the Int’l Conf. on Computer Aided Verification. Berlin:Springer-Verlag, 2010. 175–179.
[25]Finkel A. Monotonic extensions of Petri nets. Electronic Notes in Theoretical Computer Science, 2003,68(6):85–106.
[26]Ganty P, Raskin JF, Begin LV. A complete abstract interpretation framework for coverability properties of WSTS. In:Proc. of the Int’l Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin:Springer-Verlag, 2006. 49–64.
[27]GerthR,PeledD,VardiMY,etal.Simpleon-the-flyautomaticverificationoflineartemporallogic.In:ProtocolSpecification,Testing and Verification. Boston:Springer-Verlag, 1995. 3–18.
[28]Esparza J. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 1997,34(2):85–107.
[29]Murata T. Petri nets:Properties, analysis and applications. Proc. of the IEEE, 1989,77(4):541–580.