目錄

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

---

Event-B是什么？

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

• 在B方法基礎上發展出來的，基于狀態和事件的形式化系統

• 支持基于精化的模型轉換和性質證明

創始人：Prof. Jean-Raymond Abrial

Event-B形式化驗證過程

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

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

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

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

Event-B的輔助工具

Rodin平臺

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

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

可以在上面下載Rodin工具

Event-B的特點

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

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

使用數學證明來驗證不同精化級別之間的一致性

前置知識

離散數學

形式化是什么？

參見形式化基礎

我個人認為Event-B方法應該屬于形式化驗證中的定理證明

參考資料

Rodin User’s Handbook

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

Event-B & Rodin wiki

總結

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

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。