A while ago, we supported the EU project Deploy and produced a handbook for the Rodin platform, a tool for creating formal specifications using the Event-B method.  This book was a great success, but only available electronically (for free, licensed under a Creative Commons license).

Due to high demand, in particular from universities teaching formal methods, we decided to produce a print version of the handbook.  We are pleased to announce the availability of the Rodin Handbook in print – you can buy your copy at Amazon – of course, the electronic version will always be free.

What is Rodin, and Why Should I Care?

Rodin is an open source Software tool for writing formal specifications.  A formal specification uses a formal notation, instead of natural language, to describe what has to be build.  At first, this makes things more difficult: Users have to learn read and write the language.  But once this hurdle has been overcome, the result is more powerful than text:  A formal specification allows you to:

• Automatically check whether your specification is consistent.  Contradictions are detected reliably.
• Describe your system on a high, abstract level, and use refinement to produce a concrete implementation
• Automatically check whether your implementation is consistent with your specification.
• Animate or visualize your specification, even if it is abstract.
• Generate tests from your models, or even executable code.

Furthermore, many standards for safety-critical system development, like IEC 61508 or ISO 26262, recommend or even require the use of formal methods, as we reported before.

Event-B vs. Other Modeling Languages

Event-B is the formal language that is supported by Rodin.  It is a textual language and can be quite intimidating.  Most people find semi-formal languages like UML or SysML more accessible – but those languages are also less powerful.  Event-B demonstrates really well what formal languages are capable of, from theorem proving to code generation.  Therefore, we recommend Event-B and Rodin for learning about formal methods. 

Rodin also takes advantage of the Eclipse ecosystem.  Amongst many other extensions, we created an integration with ProR for requirements traceability.

Crash-Course in Formal Methods

If you need to understand formal methods, then the Rodin Handbook is a good starting point:

• The book does not require any prior knowledge of formal methods, just some basic math.
• It contains a detailed tutorial that walks you through building your first formal models, step by step.
• By following the tutorial, using the free Rodin tool, you get hands-on experience with formal methods.
• The tutorial can be completed in a few days, after which you should have a solid understanding of the subject matter.
• The extensive reference and FAQ sections of the book cover all aspects that you may encounter when writing your own formal specifications.
• If you decide to evaluate other formal or semi-formal modeling languages, knowing Event-B provides you with a solid measuring bar.

Training available

Last, we offer professional training about Formal Methods in general, and Rodin and Event-B in particular.  Please contact us if this is of interest to you.