Resumen

Las plataformas de procesamiento de permiten la manipulación y análisis de datos en tiempo real. Un sistema reconocido para este propósito es la llamada plataforma Storm, que es un sistema para computación distribuida, de código abierto, escalable, rápido y tolerante a fallos. La plataforma Storm puede ser desplegada sobre sobre un gran número de procesadores. Sin embargo, la determinación del número apropiado de procesadores que son necesarios para ejecutar adecuadamente aplicaciones de software para Storm no es una tarea fácil ni simple, especialmente si la aplicación está diseñada para ser usada por un gran número de usuarios. Una forma de resolver este problema es mediante un modelo de simulación que permita evaluar su rendimiento usando diferentes escenarios de cargas de trabajo. En este artículo, se presenta un modelo de simulación de una aplicación Storm usando el formalismo DEVS, posteriormente se define un modelo equivalente usando Autómatas Temporizados (AT). Mediante un proceso denominado “bisimulación” se comprueba que ambos modelos sean efectivamente equivalentes. Finalmente, el modelo descrito usando AT es verificado formalmente evaluando sus propiedades, demostrando que el modelo de simulación posee el mismo comportamiento que la aplicación real.

INTRODUCCIÓN

Las plataformas de procesamiento de streams están diseñadas para manejar grandes volúmenes de datos provenientes de diversas fuentes (redes sociales, publicidad, aplicaciones científicas, etc.). Estas plataformas deben procesar estos grandes volúmenes de datos en muy poco tiempo, con una latencia muy baja y un alto throughput. El procesamiento de estos datos debe ser realizado con la misma velocidad con que arriban. Una de las plataformas de procesamiento de streams más popular es Apache Storm La experimentación sobre estas plataformas en ambientes de producción resulta muy costosa, y en muchos casos, imposible debido a los riesgos de aplicar estrategias que afecten su rendimiento.

Es por este motivo que las herramientas de simulación resultan muy efectivas. Sin embargo, un simulador para que sea útil como herramienta de predicción, no sólo debe estar validado, sino que también debe estar correctamente verificado. A pesar de esto, la verificación es una tarea que muchas veces se deja de lado, aun cuando de esta forma se puede asegurar que el modelo de simulación se comporta de manera símil al sistema real.

En este trabajo, se presenta un modelo formalizado utilizando DEVS, el que luego es transformado a un modelo equivalente de Autómatas Temporizados (AT) mediante un proceso conocido como bisimulación.

• Materias:Estudio de tiempos Plataforma inteligente Ingeniería de sistemas
• Subjects:Time study Intelligent platform Systems engineering
• Palabras claves:Simulación, verificación formal, DEVS, autómatas temporizados.
• Keywords:Simulation, formal verification, DEVS, timed automaton.