B 方法是形式化方法之一，支持軟件開發(fā)的全部過程，它通過嚴(yán)格的數(shù)學(xué)推導(dǎo)和證明
來保證軟件設(shè)計和代碼的正確性。在現(xiàn)有的基本方法的基礎(chǔ)上，要想進一步提高系統(tǒng)的可靠性，需要在軟件開發(fā)中引入容錯機制，使軟件潛在的差錯對可靠性的影響縮小到最低程度。
本文將B 方法應(yīng)用于實時控制系統(tǒng)的容錯設(shè)計，并通過變配電所的饋出實時控制系統(tǒng)這一實例的研究，闡述此方法從建立初始模型，精化到最終實現(xiàn)的開發(fā)步驟。
關(guān)鍵詞：形式化方法；B 方法；容錯設(shè)計
隨著實時控制軟件在可靠性和安全性要求極高的環(huán)境和系統(tǒng)中的廣泛使用，對軟件可靠
性的依賴正在以前所未有的速度增長。目前提高軟件可靠性的一個重要的技術(shù)是容錯設(shè)計。
本文將形式化B 方法應(yīng)用于模型驅(qū)動的實時控制系統(tǒng)的開發(fā)中，逐步將容錯機制例如故障檢測，冗余技術(shù)和故障恢復(fù)融入到系統(tǒng)的規(guī)格說明和設(shè)計開發(fā)中。
B 方法是一種對軟件系統(tǒng)進行描述、設(shè)計和編碼的形式化方法[1][2]。B 方法產(chǎn)生于20 世
紀(jì)80 年代早期，在Z 語言的研究基礎(chǔ)上引入了新的技術(shù)：謂詞的轉(zhuǎn)換和Dijkstra 的最弱前
置條件。它以一種基于Zermelo-Frankle 集合論的符號表示法來書寫，使程序規(guī)格說明處于一個統(tǒng)一的數(shù)學(xué)框架下，減少了出現(xiàn)語義錯誤的可能性[3]。
本文通過變配電所系統(tǒng)這個實際項目的開發(fā)來說明容錯控制系統(tǒng)的開發(fā)步驟，由于變配
電所系統(tǒng)涉及內(nèi)容太多，為了便于分析，這里只考慮系統(tǒng)饋出（負(fù)載）的容錯設(shè)計。項目開發(fā)用的是B_Core’s BToolkit 4.0，這個工具支持軟件開發(fā)的全部過程，包括建立抽象機、精化和實現(xiàn)，語法分析，類型檢查，大部分的正確性證明以及代碼的自動生成。