Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modeling notation, the use of refinement to represent systems at different abstraction levels and the 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. The platform is open source, contributes to the Eclipse framework and is further extendible with plugins. This book provides a tutorial for new users and a reference about...

Creating a system description of high quality is still a challenging problem in the field of requirements engineering. Creating a formal system description addresses some issues. However, the relationship of the formal model to the user requirements is rarely clear, or documented satisfactorily. This work presents the ProR approach, an approach for the creation of a consistent system description from an initial set of requirements. The resulting system description is a mixture of formal and informal artefacts. Formal and informal reasoning is employed to aid in the process. To achieve this,...

ReqIF Studio is a free editor for requirements, based on the Requirements Interchange Format (ReqIF). It is based on the open source Eclipse RMF, enhanced with Essentials, the free productivity suite by Formal Mind. With ReqIF Studio, you can: (1) Manage requirements professionally. ReqIF Studio supports everything you need for professional requirements management: Arbitrary attributes of requirements, linking within and across specifications, and the ability to integrate seamlessly with other tools. (2) Directly view and edit requirements in the ReqIF format. ReqIF is an international...