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