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. 精化的功能是增加系統的功能、增加細節、改變狀態模型。精化一個自動機過程中,可能需要增加新的變數和新的事件。一般一個模型需要進行多次精化才能符合要求。

特色

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

相關詞條

熱門詞條

聯絡我們