Rodin is a free modeling tool, supporting the Event-B modeling language, for which an integration with ReqIF Studio exists. Compared with a language like UML, Event-B is much more formal.

You can access the book free online or as PDF. You can also purchase a paper version.

Who should read this book?

This book could be interesting to the following groups:

• Functional Safety Experts, who look for ways to take advantage of formal methods, as recommended by IEC 61508.
• Academics, who look for ways to integrate a formal model with requirements
• Practitioners, who want to understand the theory behind formal modeling

Note that Event-B modeling is currently only used in academia and very few highly safety-critical applications. Nevertheless, understanding a language like Event-B is a fine foundation for any other kind of modeling.