Authors
Brett Bicknell Karim Kanso
Description
The emergent discipline of using formal modelling and analysis to support industrial scale requirements engineering has matured in recent years [Woodcock et al. 2009]. This article explores Event-B–one of the more well-developed methods within this field–by means of examples and comparisons to established methods. The Event-B method and Rodin toolset allow for modelling, animation and verification of system requirements (or parts thereof), and the toolset has been largely developed by EU framework projects, notably DEPLOY and ADVANCE.