當(dāng)前位置：首頁 > 科技文檔 > 計(jì)算機(jī)軟件及計(jì)算機(jī)應(yīng)用 > 正文

基于TLA+形式化規(guī)約的Raft協(xié)議測(cè)試

軟件學(xué)報(bào) 頁數(shù)： 19 2024-02-02
摘要： Raft是最為流行的分布式共識(shí)協(xié)議之一.自2014年被提出以來, Raft協(xié)議及其變體在各種分布式系統(tǒng)中被廣泛應(yīng)用.為了證明Raft協(xié)議的正確性,開發(fā)者使用TLA+形式化規(guī)約對(duì)協(xié)議設(shè)計(jì)進(jìn)行了建模和驗(yàn)證.但由于抽象的形式化規(guī)約與實(shí)際的系統(tǒng)實(shí)現(xiàn)源碼間存在鴻溝,基于Raft實(shí)現(xiàn)的分布式系統(tǒng)中仍然會(huì)違背協(xié)議設(shè)計(jì)并引入復(fù)雜的缺陷.設(shè)計(jì)基于TLA+形式化規(guī)約的測(cè)試方法來檢測(cè)Raft協(xié)議實(shí)現(xiàn)... （共19頁）

開通會(huì)員，享受整站包年服務(wù)
科技文檔
數(shù)學(xué) 力學(xué) 化學(xué) 金融 證券 保險(xiǎn) 投資 會(huì)計(jì) 審計(jì) 園藝 林業(yè) 旅游 體育 物理學(xué) 生物學(xué) 天文學(xué) 氣象學(xué) 海洋學(xué) 地質(zhì)學(xué) 新能源 金屬學(xué) 農(nóng)藝學(xué) 農(nóng)作物 管理學(xué) 領(lǐng)導(dǎo)學(xué) 自然科學(xué) 系統(tǒng)科學(xué) 資源科學(xué) 無機(jī)化工 有機(jī)化工 燃料化工 化學(xué)工業(yè) 材料科學(xué) 礦業(yè)工程 冶金工業(yè) 安全科學(xué) 環(huán)境科學(xué) 工業(yè)通用 機(jī)械工業(yè) 無線電子 電信技術(shù) 鐵路運(yùn)輸 汽車工業(yè) 船舶工業(yè) 動(dòng)力工程 電力工業(yè) 農(nóng)業(yè)科學(xué) 農(nóng)業(yè)工程 植物保護(hù) 動(dòng)物醫(yī)學(xué) 教育理論 學(xué)前教育 初等教育 中等教育 高等教育 職業(yè)教育 成人教育 自然地理 地球物理 經(jīng)濟(jì)統(tǒng)計(jì) 農(nóng)業(yè)經(jīng)濟(jì) 工業(yè)經(jīng)濟(jì) 交通經(jīng)濟(jì) 企業(yè)經(jīng)濟(jì) 文化經(jīng)濟(jì) 信息經(jīng)濟(jì) 貿(mào)易經(jīng)濟(jì) 財(cái)政稅收 市場(chǎng)研究 科學(xué)研究 互聯(lián)網(wǎng) 自動(dòng)化 輕工業(yè) 核科學(xué) 服務(wù)業(yè) 石油然氣 服務(wù)業(yè) 野生動(dòng)物 水產(chǎn)漁業(yè) 硬件 儀器儀表 航空航天 武器軍事 公路運(yùn)輸 水利水電 建筑科學(xué) 軟件