目錄

• Event-B是什么？
• Event-B形式化驗證過程
• Event-B的輔助工具
• Event-B的特點
• 前置知識
• 形式化是什么？
• 參考資料

---

Event-B是什么？

• Event-B是一種用于系統(tǒng)級別的建模和分析的形式化方法

• 在B方法基礎(chǔ)上發(fā)展出來的，基于狀態(tài)和事件的形式化系統(tǒng)

• 支持基于精化的模型轉(zhuǎn)換和性質(zhì)證明

創(chuàng)始人：Prof. Jean-Raymond Abrial

Event-B形式化驗證過程

首先根據(jù)系統(tǒng)的需求文檔(requirements document)，使用event-b建模語言將系統(tǒng)建模為一個抽象離散模型(model)，在模型中也刻畫了對應(yīng)組件需要滿足的性質(zhì)，因為在模型狀態(tài)變化過程中，模型的某些組件可能無法滿足全局的性質(zhì)，這時候會產(chǎn)生一些需要證明的定理，我們需要證明(proof)這些定理來確保狀態(tài)變量的條件永遠(yuǎn)成立。

當(dāng)然，需要證明的定理肯定不能由我們一個個去提出來，肯定是需要相應(yīng)工具生成的，該工具稱為證明義務(wù)生成器，然后證明也應(yīng)該可以通過自動推理或者半自動推理的方式來進(jìn)行證明。

人需要的工作主要是根據(jù)需求文檔構(gòu)建相應(yīng)的模型，我們的模型肯定不是一蹴而就的，是在逐步的迭代與轉(zhuǎn)化過程中越來越完善，這種模型的迭代與轉(zhuǎn)化的過程稱為精化(refinement)，然后描述這個模型應(yīng)該滿足哪些性質(zhì)，通過定理證明的方式，證明這些個性質(zhì)是可滿足的，進(jìn)而驗證模型的正確性。

如果完成了定理的證明，我們可以說這個系統(tǒng)是相對無缺陷的(Faultless)。因為在上面的步驟中，我們相當(dāng)于構(gòu)建了一種真實軟件的近似模型，如果這個近似模型與真實軟件足夠接近，那么可以說是相對正確的，否則的話，很有可能在事先未曾預(yù)料到的外部環(huán)境出錯。

Event-B的輔助工具

Rodin平臺

它是一個基于eclipse平臺的開源IDE，對Event-B中的精化和定理證明提供了良好的支持，并且可以通過插件進(jìn)一步擴(kuò)展功能。

Rodin和Event-B的wiki主頁：https://wiki.event-b.org/index.php/Main_Page

可以在上面下載Rodin工具

Event-B的特點

使用集合論作為建模表示法

使用精化(refinement)表示不同抽象級別的系統(tǒng)

使用數(shù)學(xué)證明來驗證不同精化級別之間的一致性

前置知識

離散數(shù)學(xué)

形式化是什么？

參見形式化基礎(chǔ)

我個人認(rèn)為Event-B方法應(yīng)該屬于形式化驗證中的定理證明

參考資料

Rodin User’s Handbook

Modeling in Event-B: System and Software Engineering, J.R. Abrial (2010)

Event-B & Rodin wiki

總結(jié)

以上是生活随笔為你收集整理的Event-B建模（一）——概念与基础的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。