Verificación formal de un modelo de simulación DEVS de una aplicación Storm

Resumen

Las plataformas de procesamiento de streams permiten la manipulación y análisis de datos en tiempo real. Un sistema popular para este propósito es la plataforma Storm, un sistema de computación distribuida, escalable, rápido y tolerante a fallos. Determinar el número adecuado de procesadores para ejecutar aplicaciones Storm no es sencillo, especialmente para aplicaciones de gran escala. Este artículo presenta un modelo de simulación de una aplicación Storm usando el formalismo DEVS. Luego, se define un modelo equivalente usando Autómatas Temporizados (AT) y mediante bisimulación se verifica la equivalencia entre ambos modelos. Finalmente, se realiza la verificación formal del modelo AT, comprobando que posee el mismo comportamiento que la aplicación real.