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

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...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	Inostrosa-Psijas,Alonso, Oyarzún-Silva,Mauricio, Medina-Quispe,Fernando, García-Barrera,Francisco, Solar-Gallardo,Roberto
Lenguaje:	Spanish / Castilian
Publicado:	Universidad de Tarapacá. 2019
Materias:	Simulación verificación formal DEVS autómatas temporizados
Acceso en línea:	http://www.scielo.cl/scielo.php?script=sci_arttext&pid=S0718-33052019000400682
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

id	oai:scielo:S0718-33052019000400682
record_format	dspace
spelling	oai:scielo:S0718-330520190004006822020-01-29Verificación formal de un modelo de simulación DEVS de una aplicación StormInostrosa-Psijas,AlonsoOyarzún-Silva,MauricioMedina-Quispe,FernandoGarcía-Barrera,FranciscoSolar-Gallardo,Roberto Simulación verificación formal DEVS autómatas temporizados 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.info:eu-repo/semantics/openAccessUniversidad de Tarapacá.Ingeniare. Revista chilena de ingeniería v.27 n.4 20192019-12-01text/htmlhttp://www.scielo.cl/scielo.php?script=sci_arttext&pid=S0718-33052019000400682es10.4067/S0718-33052019000400682
institution	Scielo Chile
collection	Scielo Chile
language	Spanish / Castilian
topic	Simulación verificación formal DEVS autómatas temporizados
spellingShingle	Simulación verificación formal DEVS autómatas temporizados Inostrosa-Psijas,Alonso Oyarzún-Silva,Mauricio Medina-Quispe,Fernando García-Barrera,Francisco Solar-Gallardo,Roberto Verificación formal de un modelo de simulación DEVS de una aplicación Storm
description	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.
author	Inostrosa-Psijas,Alonso Oyarzún-Silva,Mauricio Medina-Quispe,Fernando García-Barrera,Francisco Solar-Gallardo,Roberto
author_facet	Inostrosa-Psijas,Alonso Oyarzún-Silva,Mauricio Medina-Quispe,Fernando García-Barrera,Francisco Solar-Gallardo,Roberto
author_sort	Inostrosa-Psijas,Alonso
title	Verificación formal de un modelo de simulación DEVS de una aplicación Storm
title_short	Verificación formal de un modelo de simulación DEVS de una aplicación Storm
title_full	Verificación formal de un modelo de simulación DEVS de una aplicación Storm
title_fullStr	Verificación formal de un modelo de simulación DEVS de una aplicación Storm
title_full_unstemmed	Verificación formal de un modelo de simulación DEVS de una aplicación Storm
title_sort	verificación formal de un modelo de simulación devs de una aplicación storm
publisher	Universidad de Tarapacá.
publishDate	2019
url	http://www.scielo.cl/scielo.php?script=sci_arttext&pid=S0718-33052019000400682
work_keys_str_mv	AT inostrosapsijasalonso verificacionformaldeunmodelodesimulaciondevsdeunaaplicacionstorm AT oyarzunsilvamauricio verificacionformaldeunmodelodesimulaciondevsdeunaaplicacionstorm AT medinaquispefernando verificacionformaldeunmodelodesimulaciondevsdeunaaplicacionstorm AT garciabarrerafrancisco verificacionformaldeunmodelodesimulaciondevsdeunaaplicacionstorm AT solargallardoroberto verificacionformaldeunmodelodesimulaciondevsdeunaaplicacionstorm
_version_	1714203475668107264

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

Ejemplares similares