形式化B方法驗(yàn)證技術(shù)研究及其應(yīng)用.pdf

1、形式化B方法建立在嚴(yán)格的數(shù)學(xué)基礎(chǔ)上，通過嚴(yán)格的驗(yàn)證技術(shù)證明其正確性，尤其對(duì)大型復(fù)雜系統(tǒng)的描述是非常有用和正確的。它是一種詳細(xì)規(guī)格說明、設(shè)計(jì)和系統(tǒng)編碼的方法。通過B方法來描述和驗(yàn)證能發(fā)現(xiàn)其它方法不易發(fā)現(xiàn)的系統(tǒng)描述不一致、不明確或不完整性，有助于增加軟件開發(fā)人員對(duì)系統(tǒng)的理解。實(shí)踐經(jīng)驗(yàn)告訴我們使用形式化方法的系統(tǒng)設(shè)計(jì)過程中主要的瓶頸問題就是驗(yàn)證，形式化方法的驗(yàn)證方法主要有定理證明和模型檢測。 定理證明就是從系統(tǒng)的公理出發(fā)使用推理規(guī)則逐

2、步推導(dǎo)出其所期望特性的證明過程。證明所需要的步驟依賴于系統(tǒng)的公理和推理規(guī)則。文中首先對(duì)免疫因子網(wǎng)絡(luò)的機(jī)器進(jìn)行了定理證明，從而保證了機(jī)器的正確性。 模型檢測則是對(duì)有限狀態(tài)系統(tǒng)空間進(jìn)行窮盡搜索。其主要方法為使用形式化描述語言或直接使用遷移系統(tǒng)等對(duì)系統(tǒng)進(jìn)行建模，然后進(jìn)行自動(dòng)化的連貫性檢查。這允許檢查遍及機(jī)器的所有可及的狀態(tài)，使用相應(yīng)的算法在有窮步內(nèi)自動(dòng)檢測出待檢測系統(tǒng)是否滿足待檢測性質(zhì)。模型檢測的主要缺點(diǎn)是狀態(tài)空間爆炸問題。雖然狀態(tài)空

3、間爆炸問題已經(jīng)得到一些緩解，但是一方面，由于系統(tǒng)自身內(nèi)在的非確定特性，當(dāng)系統(tǒng)所包含的可相互通訊的子系統(tǒng)數(shù)目較多時(shí)，整個(gè)系統(tǒng)規(guī)模不可避免的會(huì)增大；另一方面，系統(tǒng)所包含的數(shù)據(jù)類型有較大的值域時(shí)，不同的取值組合也會(huì)產(chǎn)生較多的狀態(tài)。無論是子系統(tǒng)的組合還是數(shù)據(jù)域的組合，都使整個(gè)狀態(tài)空間呈指數(shù)增長。條件分析是一種考慮了輸入條件之間的關(guān)系，探究輸入變量的組合的生成狀態(tài)空間的方法。我們提出將條件分析方法應(yīng)用在緩解狀態(tài)空間爆炸的問題上，該過程對(duì)需求的語義

4、進(jìn)行檢查，并將輸入和輸出之間或輸入和轉(zhuǎn)換之間的關(guān)系重新表述為邏輯關(guān)系對(duì)狀態(tài)空間進(jìn)行刪減。它考慮了輸入條件之間的關(guān)系，得到的狀態(tài)空間數(shù)目大大減少，從而緩解了狀態(tài)空間爆炸問題。 精化是B方法中的關(guān)鍵性概念。它是從高層次的規(guī)格說明開始逐步精化到實(shí)現(xiàn)，最后的實(shí)現(xiàn)可以自動(dòng)地翻譯成可執(zhí)行的代碼。精化的模型最終被精化到具有充足的實(shí)現(xiàn)細(xì)節(jié)。精化模型保證在抽象機(jī)的連續(xù)精化步驟過程中，被定義的每個(gè)不變式和前置條件都滿足。操作、不變式和前置條件生成一