Event-B

Event-B is a formal modelling language designed for rigorously modelling and verifying systems using abstraction and refinement. An Event-B model is a transition system where variables represent the state and events specify the transitions. Event-B uses a mathematical language that is based on set theory and predicate logic. Event-B is supported by the Rodin Platform, an extensible open source toolkit which includes facilities for modelling, verification (theorem proving and model checking) and validation (simulation).