Herramienta de Rodin

La herramienta Rodin es una herramienta de software para el modelado formal en Event-B . ^{[ 1 ] [ 2 ]} Fue desarrollada como parte de varios proyectos colaborativos de la Unión Europea , incluyendo inicialmente el proyecto RODIN (2004–2007). ^{[ 3 ]}

Event-B es una notación y un método desarrollados a partir del método B y está diseñado para usarse con un estilo de modelado incremental . La idea del modelado incremental se ha tomado de la programación: los lenguajes de programación modernos incluyen entornos de desarrollo integrados que facilitan la modificación y mejora de los programas. La herramienta Rodin proporciona dicho entorno para Event-B. Dos características de la herramienta Rodin son su facilidad de uso y su extensibilidad. ^{[ 2 ]}

La herramienta se centra en el modelado. Permite al usuario modificar modelos y probar variaciones de un mismo modelo. Además, es extensible. Esto posibilita adaptarla a necesidades específicas, de modo que se puede integrar en los procesos de desarrollo existentes en lugar de exigir lo contrario. Existe una wiki de Event-B asociada . ^{[ 4 ]}

Rodin ("Entorno de desarrollo abierto y riguroso para sistemas complejos") es una extensión del IDE Eclipse ( basado en Java ). El constructor de Rodin Eclipse gestiona lo siguiente: ^{[ 5 ]}

• Correctividad y verificador de tipos
• Generador de obligación de prueba (PO)
• Gestor de pruebas (GP)
• Propagación de cambios

Gerente de pruebas de Rodin (PM)

• PM construye un árbol de pruebas para cada PO
• Modos automáticos e interactivos
• PM gestiona las hipótesis utilizadas
• El PM llama a los razonadores para:
  • objetivo de descarga, o
  • dividir el objetivo en subobjetivos
• Colección de razonadores:
  • simplificador, basado en reglas, procedimientos de decisión,
• Lenguaje táctico básico para definir PM y razonadores

El proyecto Rodin incluyó cinco estudios de caso industriales que sirvieron para validar el conjunto de herramientas y ayudaron a elaborar una metodología adecuada para su uso. ^{[ 6 ]} Los estudios de caso fueron liderados por socios industriales del proyecto Rodin, con el apoyo de los demás socios. Los estudios de caso fueron los siguientes:

• Un sistema de gestión de fallos para un controlador de motor;
• Parte de una plataforma para tecnología de Internet móvil;
• Ingeniería de protocolos de comunicación;
• Un sistema de visualización de tráfico aéreo;
• Una aplicación ambiental para campus.

• Probadores de B4free ^{[ 7 ]}
  • Proveedor: ClearSy
  • Función: Demostradores de teoremas
• UML-B ^{[ 8 ]}
  • Proveedor: Universidad de Southampton
  • Función: Interfaz gráfica tipo UML para Event-B que admite diagramas de clases y diagramas de estados.
• ProB ^{[ 9 ] [ 10 ]}
  • Proveedor: Universidad de Düsseldorf
  • Función: Animación y verificación de modelos de eventos B; contraejemplos para objetivos de prueba falsos, en particular, obligaciones de prueba.
• Brama ^{[ 11 ]}
  • Proveedor: ClearSy
  • Función: Animación de modelos B. El propósito es doble:
    • Experimentación con un modelo para observar estados y transiciones.
    • Animación Flash de los modelos Event-B
• Modularización ^{[ 12 ]}
  • Proveedor: Universidad de Newcastle
  • Función: Estructurar los desarrollos del Evento B en unidades lógicas de modelado, denominadas módulos; Composición de modelos; Reutilización de modelos.

• Jean-Raymond Abrial . El libro B: Asignación de programas a significados . Cambridge University Press , 1996, ( ISBN) 0-521-49619-5).
• Jean-Raymond Abrial , Michael Butler , Stefan Hallerstede y Laurent Voisin. Un entorno de herramientas abierto y extensible para Event-B. En Z. Liu y J. He (editores), ICFEM 2006 , LNCS, volumen 4260, páginas 588-605. Springer, 2006.
• Abdolbaghi ​​Rezazadeh, Neil Evans y Michael Butler. Reurbanización de un edificio industrial: estudio de caso utilizando Event-B y Rodin. En la reunión navideña de BCS-FACS de 2007 , 2007.
• RODIN. Entregable D18: Informe intermedio sobre la evolución del estudio de caso.
• Michael Butler y Stefan Hallerstede, La herramienta de modelado formal de Rodin , Proyecto de investigación de la UE IST 511599 RODIN.
• Página principal de la plataforma Eclipse .

• Evento B y la plataforma Rodin
• Wiki de documentación de Event-B y Rodin
• Rodin en SourceForge