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.
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.