event_B是一种基于传统的谓词演算和定理证明的形式化语言。
特徵
Event-B 的新的特徵是它引入了事件( event) 。事件( event) 是Event-B的一个重要特徵，它非常适合用来为周期行为建模。，Event-B支持逐步精化地建立系统模型。
内容要点
三、event_B的基本内容和要点
- 使用event_B建模时，建立一个模型（model），一个完整的 Event－B模型应该包括场景( Context) 、自动机( Machine) 、证明义务 ( Proof Obligations ) 以及精化(Refine-ment)。
- 场景中定义静态场景和常量。集合形式的常量是载体集( Sets) ，数值形式的常量是不变数( Constants) 。在场景（Context）中用公理( Axioms) 和定理( Theo-rems)来说明常量包括载体集和不变数，以及各个常量之间的关係和它们各自的属性。
- 自动机定义系统的动态行为。每个自动机都有状态，状态由变数的值来具体体现。不变式( Invariants)规定了变数的形式及行为，而事件执行时会改变变数的值。
- 事件就是系统中可能会发生的事情，体现了动态。而事件的执行会导致系统的状态即自动机状态的变化，具体体现就是变数的值的改变。事件一般表示为:evt·any p where G( p，v) then S( p，v，v ) end( 1)其中，p 是参数，v 是变数，G( p，v) 是事件成立的条件，S( p，v，v') 是事件的行为。
- 证明义务需要证明改变后的变数的值仍然满足不变式的规定，即系统的状态仍然在安全的範围内，这样才能证明这些事件的执行是安全的。
- 精化的功能是增加系统的功能、增加细节、改变状态模型。精化一个自动机过程中，可能需要增加新的变数和新的事件。一般一个模型需要进行多次精化才能符合要求。
特色
可以在需求设计过程中保证设计的正确性和无二义性。适合于实时性强的嵌入式控制系统的建模。