Technical Specifications

• IDE: Rodin


• Supported Models: Event-B


• Platform: Eclipse


• Price: FREE


• Publisher: Event-B.org


• File Type: .exe

Key Features

• Reliable support for refinement and mathematical proof


• Requirements management


• User level syntactic and semantic extension with the Theory plug-in


• Model animation with ProB and AnimB plug-ins


• Test case generation


• Model testing

Rodin is an innovative IDE designed specifically for Event-B models. With its core development starting in 2005, this tool offers essential features for users involved in research and industrial projects where formal reasoning on models is crucial. Here are some highlighted characteristics of Rodin:

• Structural editor for open syntax models


• Built-in sequent prover for efficient proofing


• Static checker with a proof obligation generator


• Customization through a variety of plug-ins

Developed on the Eclipse platform, Rodin provides a seamless user experience with its user-friendly interface and reliable extension mechanisms. Users can also explore the standalone interface option for a personalized working environment. Additionally, Rodin allows users to package its components for customizing other Eclipse-based programs, enhancing flexibility and productivity.

For more in-depth information on Rodin's capabilities and functionalities, users can refer to the extensive documentation available on Event-B.org's wiki page.