Un enfoque declarativo para modelar el comportamiento en sistemas reactivos
El comportamiento debe contemplarse desde etapas tempranas del desarrollo de software. En este contexto el modelado declarativo incremental constituye una opción atractiva para capturar y analizar los requerimientos con precisión sin atarse a prematuras decisiones operacionales. Bajo esta visión,...
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | tesis doctoral |
| Lenguaje: | Español |
| Publicado: |
2013
|
| Materias: | |
| Acceso en línea: | http://repositoriodigital.uns.edu.ar/handle/123456789/3100 |
| Aporte de: |
| id |
I20-R126123456789-3100 |
|---|---|
| record_format |
dspace |
| institution |
Universidad Nacional del Sur |
| institution_str |
I-20 |
| repository_str |
R-126 |
| collection |
Repositorio Institucional Universidad Nacional del Sur (UNS) |
| language |
Español |
| orig_language_str_mv |
spa |
| topic |
Ciencias de la computación Ingeniería de software |
| spellingShingle |
Ciencias de la computación Ingeniería de software Asteasuain, Fernando Un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| topic_facet |
Ciencias de la computación Ingeniería de software |
| description |
El comportamiento debe contemplarse desde etapas tempranas del desarrollo
de software. En este contexto el modelado declarativo incremental constituye una opción
atractiva para capturar y analizar los requerimientos con precisión sin atarse a prematuras
decisiones operacionales. Bajo esta visión, el formalismo más utilizado son lógicas
temporales como LTL. Sin embargo, en muchas ocasiones la especificación de propiedades
en LTL es un desafío importante, aún para personas con experiencia en el formalismo.
Más aún, el poder expresivo de LTL no es suficiente si se desea construir declarativamente
un sistema desde cero a partir de las propiedades que describen su comportamiento.
Varias alternativas se han desarrollado para hacer más sencilla la especificación de
propiedades. La mayoría de ellas se basa en la utilización de patrones de especificación.
Si bien los patrones de especificación ofrecen una manera más amigable de expresar los
requerimientos típicos, el usuario necesita validar o modificar la propiedad. La evidencia
indica que para realizar todas estas tareas de validación no alcanza con analizar la descripción en lenguaje natural del patrón elegido, sino que debe analizarse su traducción a
un lenguaje formal. Y para estos casos, el usuario no tiene otra alternativa que enfrentarse
a los lenguajes formales. Luego, la utilización de patrones de especificación no logra
esconder por completo los problemas de utilizar lenguajes formales.
Este contexto sugiere la necesidad de contar con un lenguaje formal de especificación
que sea sencillo de usar, y lo suficientemente expresivo para permitir a todo tipo de
usuarios utilizarlo de manera intuitiva. Para lograr este objetivo se presenta FVS (Feather
Weight Visual Scenarios) y su extensión ω-FVS, un lenguaje declarativo, no basado en
lógicas temporales, sino en simples escenarios gráficos, cuya meta es mejorar y facilitar el
proceso de especificación de propiedades, y con el suficiente poder expresivo para denotar
propiedades ω-regulares. La notación cuenta con una semántica declarativa basada en
morfismos y un procedimiento de tableau que permite la posibilidad de realizar análisis
automático.
Se exhibe la usabilidad y aplicabilidad de FVS modelando todos los patrones de especificación, comparando las especificaciones resultantes con otras notaciones conocidas.
Tal comparación permite observar el impacto de FVS en la especificación de propiedades.
Asimismo, FVS también puede ser utilizado como un poderoso lenguaje de modelado
orientado a aspectos.
Finalmente, la extensión ω-FVS permite lograr el suficiente poder expresivo para denotar
propiedades ω-regulares. Esto se logra a través de un tipo especial de eventos,
denominados eventos fantasmas, que permiten introducir niveles de abstracción en etapas
de modelado. Se ilustra el poder expresivo de ω-FVS modelando varios ejemplos, incluyendo
protocolos de comunicación de software. ω-FVS cuenta con un proceso de síntesis,
que traduce sus especificaciones a autómatas de Buchi, permitiendo así la capacidad de
llevar a cabo diferentes tipos de razonamiento automático como consistency checking,
model checking, y oráculo para verificaci´on en ejecución entre otros. |
| author2 |
Braberman, Víctor |
| author_facet |
Braberman, Víctor Asteasuain, Fernando |
| format |
tesis doctoral |
| author |
Asteasuain, Fernando |
| author_sort |
Asteasuain, Fernando |
| title |
Un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| title_short |
Un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| title_full |
Un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| title_fullStr |
Un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| title_full_unstemmed |
Un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| title_sort |
un enfoque declarativo para modelar el comportamiento en sistemas reactivos |
| publishDate |
2013 |
| url |
http://repositoriodigital.uns.edu.ar/handle/123456789/3100 |
| work_keys_str_mv |
AT asteasuainfernando unenfoquedeclarativoparamodelarelcomportamientoensistemasreactivos |
| bdutipo_str |
Repositorios |
| _version_ |
1764820505457590274 |