LIRA

Proyecto financiado por la Xunta de Galicia (1998-2000)

En este proyecto se avanzó en el diseño y desarrollo de una herramienta software a la que hemos denominado LIRA (LOTOS Interactive Reasoning Aid) que combina las características de las FDT's no constructivas u orientadas a propiedades (lógica temporal) y de las FDT's constructivas (el trabajo está pensado para LOTOS, lenguaje de descripción formal normalizado por ISO en 1988) para proporcionar un entorno de soporte a las dos primeras fases del proceso de desarrollo.

ANTECEDENTES Y ESTADO ACTUAL

En la Ingeniería del Software el desarrollo de un sistema se lleva a cabo a través de un conjunto de fases, que definen un método de desarrollo. En estas fases se realizan visiones complementarias del sistema que lo describen en diferentes niveles de abstracción. Es necesario disponer de relaciones matemáticas claras entre estas visiones para poder integrarlas. El método de desarrollo de sistemas con FDT's suele incluir las siguientes fases:
  • Captura y especificación de requisitos. El empleo de FDT's facilitará la construcción de una descripción completa, sólida y no ambigua de los requisitos del usuario o cliente. Esta descripción constituye la arquitectura inicial del sistema.

  • Diseño de la arquitectura inicial. En esta fase se aplican un conjunto progresivo de refinamientos sobre la arquitectura inicial para incluir detalles y completar la especificación.

  • Implementación hardware/software del sistema. Esta fase suele ser semiautomática.
El éxito de un método de desarrollo está condicionado a la disposición de herramientas de soporte que liberen al diseñador de las tareas rutinarias del proceso, permitiéndole centrarse sólo en las tareas creativas.

El trabajo que se propone en el presente proyecto es continuación del iniciado por el investigador principal con el trabajo de su Tesis Doctoral. En dicho trabajo se analizó el proceso de diseño de sistemas con FDT's, en concreto con LOTOS: El desarrollo de un sistema con LOTOS suele ser un proceso de refinamientos sucesivos, es decir, el sistema se construye de forma incremental como una secuencia de pasos dirigida a obtener un producto final que satisfaga los requisitos inicialmente expresados por el cliente. En este proceso de diseño es necesario disponer de un mecanismo que permita asegurar que los efectos de los refinamientos sobre el sistema son sólo los deseados. A este respecto, en el dominio operacional de LOTOS es posible relacionar especificaciones mediantes distintos tipos de equivalencias o preórdenes. El tipo de equivalencia o preorden que se elija dependerá del tipo de refinamiento que se haya realizado. Otra posibilidad, en la que se profundizó en el trabajo de la Tesis, es demostrar la corrección de un refinamiento asegurando que el sistema (su especificación) original y el refinado satisfacen ciertas propiedades comunes. Para este propósito, se utilizó la lógica temporal para definir una sintaxis temporal para un subconjunto del lenguaje de descripción formal LOTOS (LOTOS Básico), esta sintaxis temporal ofrece las siguientes posibilidades:

  • Verificación automática de propiedades: Propiedades importantes del sistema en desarrollo pueden ser automáticamente verificadas en el dominio de la lógica temporal.

  • La especificación en lógica temporal de las propiedades de un sistema puede ser el punto de partida del desarrollo.
En paralelo con los trabajos de investigación citados anteriormente se ha desarrollado una herramienta (LIRA) cuyo objetivo es dar soporte a las dos primeras fases del ciclo de desarrollo mediante la automatización de las tareas no creativas de dicho proceso. En la actualidad, LIRA ofrece las siguientes funcionalidades básicas:
  • Edición gráfica y textual de especificaciones LOTOS. LIRA proporciona al diseñador una interfaz amigable por medio de un diagrama gráfico de bloques. Además, es posible realizar, en ambos sentidos, la traducción entre una especificación gráfica GLOTOS (Graphic-LOTOS) y una textual LOTOS, para lo cual el sistema hace previamente una verificación de la corrección sintáctica de la especificación.

  • Verificación automática de las propiedades del sistema. LIRA proporciona un algoritmo que automatiza la verificación de propiedades, expresadas en lógica temporal, del sistema.

  • Aplicación automática de transformaciones. En LIRA se definen dos clases de transformaciones:

    • Transformaciones entre unidades sintácticas LOTOS.

    • Transformaciones de propiedades. Para automatizar la aplicación de estas transformaciones, LIRA proporciona un lenguaje para expresar en reglas estas transformaciones.

  • Almacenamiento automático de la historia del desarrollo. Esta facilidad proporciona una buena ayuda a la documentación y mantenimiento de desarrollos previos.
En la actualidad, LOTOS está sometido a un proceso de revisión que previsiblemente afectará tanto a la parte de comportamiento como de datos. Este proceso de revisión dará lugar a la definición de un nuevo estándar llamado E-LOTOS (E-nhanced LOTOS).

OBJETIVOS CONCRETOS E INTERÉS DE LOS MISMOS

El objetivo básico del presente proyecto es conformar un marco de trabajo que, aprovechando la experiencia acumulada, permita incrementar la utilidad y eficacia del entorno LIRA, ofreciendo nuevas funcionalidades y consolidando las ya existentes. Con el objeto de darle al trabajo una proyección de futuro es preciso tener en cuenta que el lenguaje de descripción formal LOTOS está en la actualidad en proceso de revisión, estimándose que las propuestas de modificación y mejora del lenguaje serán estables en breve. Con estas premisas, para la consecución del objetivo básico planteado es necesario orientar el trabajo en las siguientes direcciones:
  • Actualización y adaptación de las funcionalidades del entorno a la nueva versión del lenguaje (E-LOTOS).

  • En la actualidad, el proceso de desarrollo de un sistema comienza en LIRA cuando se dispone de la arquitectura inicial del sistema. Cuando no se dispone de un estándar como punto de partida del diseño del sistema, se hace necesario que la herramienta proporcione un formalismo para la captura y especificación de los requisitos de dicho sistema. La definición e implementación de este formalismo es uno de los objetivos que se plantean en este proyecto para incrementar la utilidad del entorno.

  • La facilidad de verificación automática de propiedades que proporciona LIRA sólo contempla un subconjunto de LOTOS (LOTOS Básico) que no contiene tipos de datos. La posibilidad de extender la verificación de propiedades a todo el lenguaje LOTOS constituye asimismo una mejora importante del entorno que pensamos abarcar en este proyecto.

  • La extensión del algoritmo de verificación a todo el lenguaje LOTOS permitirá introducir nuevos mecanismos de verificación en el proceso de desarrollo transformacional: Se puede condicionar la aplicación de transformaciones entre unidades sintácticas LOTOS a que la especificación original y la trasformada satisfagan ciertas propiedades comunes.

  • El formalismo de captura y especificación de requisitos permitirá abordar el mantenimiento de especificaciones a nivel de requisitos, lo que supone el diseño, orientado a la reutilización de especificaciones con subconjuntos de requisitos comunes, de las estructuras a almacenar.

METODOLOGÍA, HIPÓTESIS Y PLAN DE TRABAJO

Los objetivos planteados en el presente proyecto son de dos tipos: Unos orientados a consolidar las funcionalidades existentes en LIRA y adaptarlas a la nueva versión del lenguaje (E-LOTOS), y otros orientados al diseño e implementación de nuevas funcionalidades. Para la consecución de los objetivos citados en primer lugar se seguirá el siguiente plan de trabajo:
  • Estudio detallado de las modificaciones y nuevas funcionalidades del lenguaje E-LOTOS.

  • Adaptación de la interfaz de usuario a E-LOTOS. Esta tarea supondrá la revisión y actualización del editor gráfico, del editor textual, del traductor entre especificaciones gráficas y textuales, y del analizador sintáctico.

  • Adaptación de la semántica temporal definida en LIRA a la nueva versión del lenguaje, y modificación y mejora de los algoritmos de verificación de propiedades.

  • Adaptación del algoritmo de aplicación automática de reglas de transformación. Para realizar esta adaptación será necesario reconsiderar la sintaxis y la expresividad del lenguaje de definición de reglas.
El plan de trabajo propuesto para el conjunto de objetivos citados en segundo lugar es el siguiente:
  • Formalismo de captura y especificación de requisitos: Utilización de FDT's orientadas a propiedades para la definición de este formalismo. Se comenzará el trabajo con una lógica temporal causal, no incluyendo inicialmente tipos de datos. Inclusión de tipos de datos en el formalismo de especificación de requisitos.

  • Para la extensión de la verificación automática de propiedades a todo el lenguaje se seguirán los siguientes pasos:

    • Estudio detallado de los nuevos tipos de datos de E-LOTOS.

    • Estudio, implementación y prueba de un algoritmo de verificación restringido a tipos de datos finitos (booleanos, etc.).

    • Estudio de la posibilidad de ampliación del algoritmo anterior a otros tipos de datos.

  • Diseño e implementación de algoritmos de almacenamiento que faciliten la reutilización de especificaciones a nivel de requisitos.