一種基于分離邏輯的塊云存儲(chǔ)系統(tǒng)驗(yàn)證工具

摘要： 云存儲(chǔ)技術(shù)目前被廣泛應(yīng)用于人們的生產(chǎn)與生活中.驗(yàn)證云存儲(chǔ)系統(tǒng)中管理程序的正確性,能夠有效地提高整個(gè)系統(tǒng)的可靠性.塊云存儲(chǔ)系統(tǒng)(CBS)具有最接近底層的存儲(chǔ)架構(gòu).運(yùn)用交互式定理證明器Coq,實(shí)現(xiàn)了一種輔助驗(yàn)證工具,用于分析和驗(yàn)證CBS中管理程序的正確性.基于分離邏輯的思想,對工具中證明系統(tǒng)的實(shí)現(xiàn)主要包括:首先,將CBS抽象為兩層堆結(jié)構(gòu),定義建模語言形式化表示CBS的狀態(tài)和管理程序...