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. / Behavior needs to be understood from early stages of software development. In this
context incremental and declarative modeling seems an attractive approach for closely
capturing and analyzing requirements without early operational commitment. In this situation,
the most widespread formalism is LTL (Linear Temporal Logic). Unfortunately, in
many cases, the formal description and validation of properties results in a daunting task,
even for trained people. Moreover, LTL expressive power fall short of if the practitioner
want to declaratively build a system from scratch upon the specified properties.
Several attempts arise to make life easier for practitioners, in order to circumvent the
complexity involved when specifying properties in LTL. The purpose of these approaches
is to provide to the user an easier way to express the desired behavior. Most of them
rely on specification patterns. Although patterns offer a friendlier way to express typical
requirements, the user still needs to validate or modify the property. However, to perform
all these validations tasks based solely on the natural language description of the patterns
may be hard to achieve and many times the pattern translation into an formalism must
be analyzed instead. Besides, sometimes a property needs to be slightly modified to suit
actual system requirements, and this, again, suggests manipulations of the translated
versions. Therefore, using patterns is not enough to entirely hide the subtleties of the
underlying formalism from the user.
This suggests the need of a formal specification language easy to use, and sufficiently
expressive to enable skilled and non-skilled users to use it appropriately, which constitutes
the main objective of this work. To achieve this goal we present FVS (Feather Weight Visual
Scenarios) and its extension ω-FVS, a declarative language, not founded on temporal
logics, but on simple graphical scenarios, which aims to improve and ease the property
specification process, and powerful enough to express omega-regular properties. The notation
is equipped with declarative semantics based on morphisms and a tableau procedure
iv
is given enabling the possibility of automatic analysis.
We illustrate FVS applicability by modeling all the specification patterns and we
thoroughly compare FVS to other known approaches, showing that FVS specifications
are better suited for validation tasks. What is more, FVS is presented as a useful aspectoriented
modeling language.
In addition, we present ω-FVS, a simple extension of FVS capable of expressing ω-
regular properties. This feature is achieved by introducing a distinctive type of events,
called “ghost” events, that allow to predicate behavior in a higher level of abstraction.
We illustrate ω-FVS expressive power by modeling several examples, including real world
protocols specifications. On the top of these features, we also developed a synthesis procedure
which translates FVS specifications into Buchi automata, enabling the possibility
for different sort of analysis, namely consistency checking, model checking, and oracle for
runtime verification among others.
| Identifer | oai:union.ndltd.org:uns.edu.ar/oai:repositorio.bc.uns.edu.ar:123456789/3100 |
| Date | 20 December 2013 |
| Creators | Asteasuain, Fernando |
| Contributors | Braberman, Víctor, Fillottrani, Pablo Rubén |
| Publisher | Universidad Nacional del Sur |
| Source Sets | Universidad Nacional del Sur |
| Language | Spanish |
| Detected Language | Spanish |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0057 seconds