Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract)
作者： Patrice Godefroid , Didier Pirottin
关键词:
摘要: Partial-order verification methods exploit “independency” between transitions of a concurrent program to avoid parts the state space explosion due modeling concurrency by interleaving. In this paper, we study influence refining dependencies on effectiveness these methods. We show that carefully tracking can yield substantial improvements for their performances. For instance, were able decrease memory requirements needed real-size protocol with such method from factor 5 25 only dependencies.
springer.com
sci-hub.st 参考文章(17)
Claude Jard, Thierry Jeron, On-line model checking for finite linear temporal logic specifications computer aided verification. ,vol. 407, pp. 189- 196 ,(1989) , 10.1007/3-540-52148-8_16
Patrice Godefroid, Gerard J. Holzmann, Didier Pirottin, State-Space Caching Revisited computer aided verification. pp. 178- 191 ,(1992) , 10.1007/3-540-56496-9_15
David K. Probst, Hon F. Li, Using Partial-Order Semantics to Avoid the State Explosion Problem in Asynchronous Systems computer aided verification. pp. 146- 155 ,(1990) , 10.1007/BFB0023728
Doron Peled, All from One, One for All: on Model Checking Using Representatives computer aided verification. pp. 409- 423 ,(1993) , 10.1007/3-540-56922-7_34
Patrice Godefroid, Using Partial Orders to Improve Automatic Verification Methods computer aided verification. pp. 176- 185 ,(1990) , 10.1007/BFB0023731
Gerard J. Holzmann, Patrice Godefroid, Didier Pirottin, Coverage Preserving Reduction Strategies for Reachability Analysis Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification XII. pp. 349- 363 ,(1992) , 10.1016/B978-0-444-89874-6.50028-3
Edward Ochmański, Semi-Commutation and Deterministic Petri Nets mathematical foundations of computer science. pp. 430- 438 ,(1990) , 10.1007/BFB0029639
William T. Overman, Stephen D. Crocker, Verification of Concurrent Systems: Function and Timing Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 401- 409 ,(1982)
Antti Valmari, A Stubborn Attack On State Explosion computer aided verification. ,vol. 1, pp. 156- 165 ,(1990) , 10.1007/BF00709154
Patrice Godefroid, Pierre Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties computer aided verification. ,vol. 2, pp. 332- 342 ,(1991) , 10.1007/BF01383879