EB2Python - Traducción automática de especificaciones Event-B en Rodin a Python

Event-B es un metodo formal para el modelado y analisis de sistemas basado en el enfoque de correccion por construccion. Presenta un conjunto de teorias como la eleccion para la notacion de modelado, el refinamiento para representar diferentes niveles de abstraccion en los modelos y un sistema de prueba para verificar la consistencia dichos modelos. Este documento presenta una algoritmo para generar programas en el lenguaje de programacion Python a partir de modelos Event-B correctos. El algoritmo presentado aqui es la composicion de reglas de traduccion; incluye soporte para relaciones, expresiones numericas y enumeraciones. El codigo puede ser generado para ejecucion secuencial o concurrente (por medio de hilos). Un ejemplo ilustra la traduccion de codigo y su ejecucion como programa en el lenguaje de programacion Python.