event_B

event_B是一種基於傳統的謂詞演算和定理證明的形式化語言。

特徵

Event-B 的新的特徵是它引入了事件( event) 。事件( event) 是Event-B的一個重要特徵，因此它非常適合用來為周期行為建模。另外，Event-B支持逐步精化地建立系統模型。

內容要點

三、event_B的基本內容和要點

1. 使用event_B建模時，首先建立一個模型（model），一個完整的 Event－B模型應該包括場景( Context) 、自動機( Machine) 、證明義務 ( Proof Obligations ) 以及精化(Refine-ment)。
2. 場景中定義靜態場景和常量。集合形式的常量是載體集( Sets) ，數值形式的常量是不變數( Constants) 。在場景（Context）中用公理( Axioms) 和定理( Theo-rems)來說明常量包括載體集和不變數，以及各個常量之間的關係和它們各自的屬性。
3. 自動機定義系統的動態行為。每個自動機都有狀態，狀態由變數的值來具體體現。不變式( Invariants)規定了變數的形式及行為，而事件執行時會改變變數的值。
4. 事件就是系統中可能會發生的事情，體現了動態。而事件的執行會導致系統的狀態即自動機狀態的變化，具體體現就是變數的值的改變。事件一般表示為:evt·any p where G( p，v) then S( p，v，v ) end( 1)其中，p 是參數，v 是變數，G( p，v) 是事件成立的條件，S( p，v，v') 是事件的行為。
5. 證明義務：需要證明改變後的變數的值仍然滿足不變式的規定，即系統的狀態仍然在安全的範圍內，這樣才能證明這些事件的執行是安全的。
6. 精化的功能是增加系統的功能、增加細節、改變狀態模型。精化一個自動機過程中，可能需要增加新的變數和新的事件。一般一個模型需要進行多次精化才能符合要求。

特色

可以在需求設計過程中保證設計的正確性和無二義性。適合於實時性強的嵌入式控制系統的建模。