herramienta rodin

Modelado en el Evento-B

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

Descripción general

Event-B es una notación y un método desarrollado a partir del método B y está diseñado para usarse con un estilo incremental de modelado . La idea del modelado incremental se tomó de la programación: los lenguajes de programación modernos vienen con un entorno de desarrollo integrado que facilita 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 modelo. La herramienta también es extensible. Esto hace posible adaptar la herramienta a necesidades específicas, de modo que la herramienta se pueda adaptar para encajar en los procesos de desarrollo existentes en lugar de exigir lo contrario. Hay un wiki Event-B asociado . ^[4]

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

• Bien formado y corrector de tipos.
• Generador de obligación de prueba (PO)
• Gerente de pruebas (PM)
• Propagación de cambios

Gerente de pruebas de Rodin (PM)

• PM construye un árbol de prueba para cada PO
• Modos automáticos e interactivos.
• PM gestiona las hipótesis utilizadas.
• PM llama a los razonadores a:
  • objetivo de descarga, o
  • dividir el objetivo en subobjetivos
• Colección de razonadores:
  • procedimientos de decisión más simplificados y basados ​​en reglas,
• Lenguaje de tácticas básicas para definir PM y razonadores.

Aplicaciones industriales y estudios de casos.

El proyecto Rodin incluyó cinco estudios de casos industriales que sirvieron para validar el conjunto de herramientas y ayudaron a elaborar una metodología adecuada para utilizarlas. ^[6] Los estudios de caso fueron dirigidos 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 comunicaciones;
• Un sistema de visualización del tráfico aéreo;
• Una aplicación ambiental del campus.

Algunos complementos disponibles para Rodin

• Probadores B4free ^[7]
  • Proveedor: ClearSy
  • Función: demostradores de teoremas
• UML-B ^[8]
  • Proveedor: Universidad de Southampton
  • Función: interfaz gráfica similar a UML para diagramas de clases y gráficos de estado compatibles con Event-B
• ProB ^{[9] [10]}
  • Proveedor: Universidad de Düsseldorf
  • Función: Animación y verificación de modelos de Eventos-B; Contraejemplos de objetivos de prueba falsa, 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 modelos Event-B
• Modularización ^[12]
  • Proveedor: Universidad de Newcastle
  • Función: Estructurar los desarrollos del Evento-B en unidades lógicas de modelado, llamadas módulos; Composición del modelo; Reutilización de modelos

Referencias

1. Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta y Laurent Voisin. (2010). "Rodin: un conjunto de herramientas abierto para modelar y razonar en Event-B". Revista Internacional sobre Herramientas de Software para la Transferencia de Tecnología . 12 : 447–466. doi :10.1007/s10009-010-0145-y.{{cite journal}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )
2. Butler, Michael y Stefan Hallerstede (2007). La herramienta de modelado formal de Rodin (PDF) . FACS 2007 Taller de Navidad: Métodos Formales en la Industria . págs. 1 a 5.{{cite conference}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )
3. "RODIN: entorno de desarrollo abierto riguroso para sistemas complejos". Reino Unido: Universidad de Newcastle . Consultado el 13 de junio de 2023 .
4. "Wiki de documentación de Event-B y Rodin". wiki.event-b.org . Consultado el 13 de junio de 2023 .
5. Mayordomo, Michael . "RODIN: las herramientas de perfeccionamiento de próxima generación" (PDF) . Reino Unido: Universidad de Southampton . Consultado el 13 de junio de 2023 .
6. "Proyecto IST-511599 RODIN" Entorno de desarrollo abierto riguroso para sistemas complejos"" (PDF) . Reino Unido: Universidad de Newcastle . Consultado el 13 de junio de 2023 .
7. "B4free como herramienta gratuita para todos". Claro . Consultado el 13 de junio de 2023 .
8. "UML-B: lenguaje de modelado de sistemas confiable". uml-b.org . Consultado el 13 de junio de 2023 .
9. "¿Qué es ProB?". prob.hhu.de. ​Alemania: Universidad de Düsseldorf . Consultado el 13 de junio de 2023 .
10. Leonova, Mariya Aleksandrovna y Petr Nikolaevich Devyanin (2022). "Comparación de métodos para modelar el control de acceso en SO y DBMS en Event-B para su verificación con herramientas Rodin y ProB". Prikladnaya Diskretnaya Matematika . Suplemento 15: 90–99. doi :10.17223/2226308X/15/22.{{cite journal}}: Mantenimiento CS1: varios nombres: lista de autores ( enlace )
11. "El animador Brama de RODIN". ResearchGate.net . Consultado el 13 de junio de 2023 .
12. "Complemento de modularización". wiki.event-b.org . Consultado el 13 de junio de 2023 .

Otras lecturas

• Jean-Raymond Abrial . El B-Book: Asignación de significados a programas . Prensa de la Universidad de Cambridge , 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 una industria, estudio de caso utilizando Event-B y Rodin. En Reunión de Navidad 2007 de BCS-FACS , 2007.
• RODÍN. Entregable D18: Informe intermedio sobre desarrollos de estudios 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 de inicio de la plataforma Eclipse.

enlaces externos

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