Preface

Nobody likes to write documentation, yet everybody agrees that documentation is crucially important. For a tool platform as complex as Rodin, documentation is necessary if it is supposed to succeed in reaching a wider audience.

The executive team of the DEPLOY project recognized this. In a meeting at ETH in 2010, the team established, amongst other things, that “it is clear that the current documentation would not support, say, an engineer in an automotive company to start using the tools without significant support”. It then commissioned the creation of better Rodin documentation. This handbook is the result of this effort.

Rather than reinventing the wheel, we took all the existing documentation into account, restructured it, extended it where necessary, created plenty of cross-references, and put the resulting document through an editorial process to ensure readability.

A word of warning and encouragement: Don’t expect to be an expert in Event-B modelling after reading this handbook. Its aim is to provide support while getting acquainted with the tool platform. It provides the basics of modelling and can also be used as a companion guide for experts. Beginners can work their way through the tutorial, which starts with installation and ends with moderately difficult proofs. Additional support is available in the form of an FAQ and a comprehensive index. Advanced users can refer to the comprehensive reference section, where they can quickly find essential information regarding the different formalisms.

Whenever the handbook requires former knowledge, it provides links and hints about where to get it. Whenever it stops, it provides references for further reading. In particular, it provides plenty of references to the Rodin Wiki, and provides information on how to get in touch with the Rodin community. We are confident that this handbook will achieve its mission to get new users acquainted with Rodin without frustration and hopefully some with fun.

Michael Jastram, Düsseldorf, 2012