%0 Conference Paper %1 1495122 %A Minamikawa, Takahiro %A Tsuchiya, Tatsuhiro %A Kikuno, Tohru %B PRDC '08: Proceedings of the 2008 14th IEEE Pacific Rim International Symposium on Dependable Computing %C Washington, DC, USA %D 2008 %I IEEE Computer Society %K consensus homodel modelchecking tool %P 40--47 %R 10.1109/PRDC.2008.13 %T Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms %U http://portal.acm.org/citation.cfm?id=1495122 %X Model checking is a successful formal verification technique; however, its application to fault-tolerant distributed algorithms is still not common practice. One major reason for this is that model checking requires non-negligible users’ efforts in representing the algorithm to be verified in the input language of a model checker. To alleviate this problem we propose an approach which encompasses (i) a language for concisely describing fault-tolerant distributed algorithms and (ii) a translator from the proposed language to PROMELA, the input language of the SPIN model checker. To demonstrate the feasibility of our approach, we show the results of an experiment where we described and verified several algorithms for consensus, a well-known distributed agreement problem. %@ 978-0-7695-3448-0

@inproceedings{1495122, abstract = {Model checking is a successful formal verification technique; however, its application to fault-tolerant distributed algorithms is still not common practice. One major reason for this is that model checking requires non-negligible users’ efforts in representing the algorithm to be verified in the input language of a model checker. To alleviate this problem we propose an approach which encompasses (i) a language for concisely describing fault-tolerant distributed algorithms and (ii) a translator from the proposed language to PROMELA, the input language of the SPIN model checker. To demonstrate the feasibility of our approach, we show the results of an experiment where we described and verified several algorithms for consensus, a well-known distributed agreement problem.}, added-at = {2010-03-24T18:06:56.000+0100}, address = {Washington, DC, USA}, author = {Minamikawa, Takahiro and Tsuchiya, Tatsuhiro and Kikuno, Tohru}, biburl = {https://www.bibsonomy.org/bibtex/23b828a30ff040af350c05adcee0c580f/giuliano.losa}, booktitle = {PRDC '08: Proceedings of the 2008 14th IEEE Pacific Rim International Symposium on Dependable Computing}, description = {Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms}, doi = {10.1109/PRDC.2008.13}, interhash = {6e3b32c93a3bb0f87f7ec8b09a47a41e}, intrahash = {3b828a30ff040af350c05adcee0c580f}, isbn = {978-0-7695-3448-0}, keywords = {consensus homodel modelchecking tool}, pages = {40--47}, publisher = {IEEE Computer Society}, timestamp = {2010-03-24T18:06:56.000+0100}, title = {Language and Tool Support for Model Checking of Fault-Tolerant Distributed Algorithms}, url = {http://portal.acm.org/citation.cfm?id=1495122}, year = 2008 }