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

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

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

開通會員，享受整站包年服務(wù)