Parameterized model checking of fault-tolerant distributed algorithms by abstraction
作者： Annu John , Igor Konnov , Ulrich Schmid , Helmut Veith , Josef Widder
DOI: 10.1109/FMCAD.2013.6679411
关键词:
摘要: We introduce an automated parameterized verification method for fault-tolerant distributed algorithms (FTDA). FTDAs are parameterized by both the number of processes and the …
researchgate.net 
arise.or.at 参考文章(35)
Bernadette Charron-Bost, Stephan Merz, Formal Verification of a Consensus Algorithm in the Heard-Of Model International Journal of Software and Informatics. ,vol. 3, pp. 273- 303 ,(2009)
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder, Towards Modeling and Model Checking Fault-Tolerant Distributed Algorithms international workshop on model checking software. pp. 209- 226 ,(2013) , 10.1007/978-3-642-39176-7_14
Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta, Program analysis using symbolic ranges static analysis symposium. pp. 366- 383 ,(2007) , 10.1007/978-3-540-74061-2_23
K. L. McMillan, Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking Lecture Notes in Computer Science. pp. 179- 195 ,(2001) , 10.1007/3-540-44798-9_17
E. Allen Emerson, Vineet Kahlon, Exact and Efficient Verification of Parameterized Cache Coherence Protocols Lecture Notes in Computer Science. pp. 247- 262 ,(2003) , 10.1007/978-3-540-39724-3_22
Gerard J. Holzmann, The SPIN Model Checker ,(2003)
Edmund Clarke, Murali Talupur, Helmut Veith, Proving ptolemy right: the environment abstraction framework for model checking concurrent systems tools and algorithms for construction and analysis of systems. pp. 33- 47 ,(2008) , 10.1007/978-3-540-78800-3_4
Igor Konnov, Josef Widder, Helmut Veith, Annu John, Ulrich Schmid, Counter Attack on Byzantine Generals: Parameterized Model Checking of Fault-tolerant Distributed Algorithms arXiv: Logic in Computer Science. ,(2012)
Dana Fisman, Orna Kupferman, Yoad Lustig, On verifying fault tolerance of distributed protocols tools and algorithms for construction and analysis of systems. pp. 315- 331 ,(2008) , 10.1007/978-3-540-78800-3_22
E. Allen Emerson, Vineet Kahlon, Reducing Model Checking of the Many to the Few conference on automated deduction. pp. 236- 254 ,(2000) , 10.1007/10721959_19