LIRA (1998-2000) 
Proyecto financiado por la Xunta de Galicia.
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.
