A formal method for system-level modelling and analysis
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.
set theory as a modelling notation
use of refinement to represent systems at different abstraction levels
use of mathematical proof to verify consistency between refinement levels
The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof