基于B方法的實(shí)時(shí)控制系統(tǒng)的容錯(cuò)設(shè)計(jì)

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