Event-B

A formal method for system-level modelling and analysis

Software Modelling

Software defects result in a lot of time-consuming test and fix of software and, if left undetected, have a detrimental impact on software users. A significant proportion of software defects arise in requirements and design phases but are only detected after coding phases when software is being tested or deployed. The use of formal modelling to clearly specify and analyse requirements and designs helps to eliminate many defects prior to coding.

Feature List

  • modelling notation

    set theory as a modelling notation

  • refinement

    use of refinement to represent systems at different abstraction levels

  • proof

    use of mathematical proof to verify consistency between refinement levels

  • tool support

    The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof

Quick start

start with Rodin tool set

Rodin Handbook