La herramienta Rodin es una herramienta para el modelado formal en Event-B. Event-B es una notación y un método desarrollado a partir del Método B y está destinado a ser utilizado con un estilo de modelado incremental . La idea del modelado incremental se ha tomado de la programación: los lenguajes de programación modernos vienen con un entorno de desarrollo integradoque facilitan la modificación y mejora de programas. La herramienta Rodin proporciona un entorno de este tipo para Event-B. Las dos características principales de la herramienta Rodin son su facilidad de uso y su extensibilidad. La herramienta se centra en el modelado. Es fácil modificar modelos y probar variaciones de un modelo. La herramienta también se puede extender fácilmente. Esto permite adaptar la herramienta a necesidades específicas, por lo que la herramienta se puede adaptar para encajar en los procesos de desarrollo existentes en lugar de exigir lo contrario. La wiki de Event-B es un recurso útil para usuarios y desarrolladores.
Rodin (Entorno de desarrollo abierto riguroso para sistemas complejos) es una extensión de Eclipse IDE (basado en Java). Coordenadas de Rodin Eclipse Builder:
El proyecto Rodin incluyó cinco estudios de casos industriales que sirvieron para validar el conjunto de herramientas y ayudaron en la elaboración de una metodología adecuada para el uso de las herramientas. Los estudios de caso fueron dirigidos por socios industriales del proyecto Rodin apoyados por los otros socios. Los estudios de caso fueron los siguientes: