共識(shí)協(xié)議的形式化驗(yàn)證研究現(xiàn)狀與展望

摘要： 分布式系統(tǒng)在計(jì)算環(huán)境中發(fā)揮重要的作用,其中的共識(shí)協(xié)議算法用于保證節(jié)點(diǎn)間行為的一致性.共識(shí)協(xié)議的設(shè)計(jì)錯(cuò)誤可能導(dǎo)致系統(tǒng)運(yùn)行故障,嚴(yán)重時(shí)可能對(duì)人員和環(huán)境造成災(zāi)難性的后果,因此保證共識(shí)協(xié)議設(shè)計(jì)的正確性非常重要.形式化驗(yàn)證能夠嚴(yán)格證明設(shè)計(jì)模型中目標(biāo)性質(zhì)的正確性,適合用于驗(yàn)證共識(shí)協(xié)議.然而,隨著分布式系統(tǒng)的規(guī)模增大,問題復(fù)雜度提升,使得分布式共識(shí)協(xié)議的形式化驗(yàn)證更為困難.采用什么方法對(duì)共識(shí)...