Soporte metodológico para la evolución de especificaciones formales. Aplicación en sistemas telemáticos

Resumen

El tránsito hacia la denominada Sociedad de la Información está transformando de manera notoria los principios de la ingeniería telemática. Nuevos dispositivos, nuevos esquemas de comunicación y nuevos servicios dibujan un escenario considerablemente más complejo que el de la comunicación cliente-servidor entre ordenadores, los sistemas monousuario y la computación centralizada. Esa mayor complejidad se pone de manifiesto tanto en tiempo de diseño de los sistemas como durante su funcionamiento: por una parte, la dificultad para anticipar todas las características de un sistema obliga a plantear el desarrollo como un proceso de continua revisión hasta llegar a la solución deseada; por otra, las nuevas aplicaciones y formas de comunicación exigen formas de adaptar las redes a las condiciones que se observen y los objetivos que se fijen en cada momento. El objetivo de esta tesis es dar solución a un conjunto de problemas observados en el manejo de especificaciones formales de sistemas telemáticos. Tales especificaciones son la base para cualquier soporte automatizado que se quiera proporcionar en la definición (en tiempo de desarrollo o en tiempo de operación) de lo que debe hacer o de cómo debe ser un sistema. La cuestión principal es que rara vez se dispone de una idea completa y correcta de la funcionalidad deseada para un sistema y de los objetivos que éste debe satisfacer; así, surge la necesidad de realizar cambios en las especificaciones, ya sea para completar un conocimiento parcial o para corregir contradicciones y desalineamientos con respecto a los objetivos. A este respecto, los trabajos anteriores no prestan un soporte eficaz para lo que es una labor eminentemente creativa. A menudo se ha tratado de automatizar todo el proceso de detección de errores y modificación de las especificaciones, sin considerar las múltiples posibilidades de evolución que se dan en un caso general y sin informar adecuadamente de los cambios a los agentes involucrados en la elaboración de las mismas. También existen limitaciones a la hora de hacer abordable la complejidad de los sistemas, que inciden en el razonamiento sobre los cambios que se requieren en cualquier etapa. En esta tesis se propone un esquema para la elaboración de especificaciones formales, concebido en torno ala necesidad de afrontar frecuentes cambios en bases de conocimiento parciales y posiblemente incorrectas. El núcleo de dicho esquema toma la forma de un ciclo de dos fases: análisis y revisión, donde cualesquiera problemas detectados sobre una especificación se traducen automáticamente en sugerencias de revisión fácilmente entendibles por los agentes que la elaboran. Esa base se complementa con mecanismos destinados a promover un razonamiento intuitivo y focalizado. El esquema completo se ha validado en dos dominios de aplicación representativos de los nuevos escenarios que se plantean en el desarrollo y en el funcionamiento de sistemas telemáticos: la especificación de patrones de interacción en sistemas interactivos multiusuario, y la planificación de la provisión de servicios en redes ad hoc de dispositivos móviles. En el primer caso, el ciclo de análisis-revisión ha permitido implementar un entorno que mejora los enfoques existentes en la aplicación de técnicas formales al desarrollo de sistemas interactivos, gracias a la definición de un proceso software iterativo que facilita la labor creativa de los desarrolladores. En el caso de las redes ad hoc, el ciclo de análisis-revisión se ha constituido como el núcleo de un esquema de coordinación en el que múltiples dispositivos móviles, explotando un conocimiento parcial de un entorno altamente cambiante, colaboran en el objetivo de conformar la red que mejor satisface sus necesidades de servicio._