Un enfoque declarativo para modelar el comportamiento en sistemas reactivos

Abstract

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.