کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4951769 | 1441600 | 2017 | 23 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Distributed programs are known to be extremely difficult to implement, test, verify, and maintain. This is due in part to the large number of possible unforeseen interactions among components, and to the difficulty of precisely specifying what the programs should accomplish in a formal language that is intuitively clear to the programmers. We discuss here a methodology that has proven itself in building a state of the art implementation of Multi-Paxos and other distributed protocols used in a deployed database system. This article focuses on the logical foundations as well as the basic ideas of formal EventML programming, illustrated by implementing a fault-tolerant consensus protocol and showing how we prove its safety properties with the Nuprl proof assistant.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 148, 15 November 2017, Pages 26-48
Journal: Science of Computer Programming - Volume 148, 15 November 2017, Pages 26-48
نویسندگان
Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable,