Motivación

La fiabilidad en la construcción de software se ha convertido en una necesidad reconocida, no sólo en el nuevo programa nacional de Tecnologías Informáticas, sino también en las industrias de desarrollo de software. Con el crecimiento de los sistemas de software, que han evolucionado hasta alcanzar tamaños y complejidades extraordinariamente altos, su inestabilidad se está convirtiendo, lamentablemente, en algo cotidiano y asumido con resignación por los usuarios en una sociedad de la información cada vez más exigente. Para garantizar esta fiabilidad son necesarias técnicas, métodos y herramientas que soporten de forma adecuada el proceso de desarrollo y, para esto, se necesita una inversión de recursos que promueva avances en la investigación de nuevos métodos de desarrollo de software, nuevas técnicas de verificación y validación, nuevas tecnologías de soporte para componentes de software comercial, etc.

Sin embargo, uno de los inconvenientes que ha presentado tradicionalmente la investigación sobre métodos formales en la Informática ha sido la dificultad para realizar una transferencia tecnológica de resultados a la industria. Esta dificultad se debe, en gran parte, al alto coste que supone una verificación formal completa y que, a excepción de los entornos de seguridad crítica, en los demás resulta prohibitivo. Por lo tanto, el coste de la especificación debe reducirse drásticamente y el análisis debe automatizarse pues, de otro modo, la industria no encontrará razones para la adopción de los métodos formales. Con los métodos formales existentes, cuando se usan de forma convencional, no se pueden alcanzar estos objetivos; en cambio, un método formal "ligero" ( lightweight), que enfatice la parcialidad y la aplicación focalizada, puede traer grandes beneficios a un coste reducido.

El término lightweight se hizo popular a finales de los años 90 para referirse a métodos de desarrollo alternativos a los habitualmente propuestos en el campo de la Ingeniería del Software, aunque ya fue acuñado a mediados de los 90 para referirse al uso parcial de los métodos formales. La idea fundamental de estos métodos, que comenzaron a denominarse ágiles, es la eliminación del exceso de "burocracia" tradicionalmente implícita en la aplicación de las metodologías, promoviendo su agilización (en estas páginas se ha optado por utilizar también el término "ágil" para hacer referencia a este enfoque). Como se defiende en estos métodos formales deben satisfacer ciertos requisitos a nivel de lenguaje, de modelado, de análisis y de composición con respecto a la parcialidad que caracteriza a este enfoque:

  • Parcialidad en el lenguaje. Hasta ahora los lenguajes de especificación se han juzgado principalmente por su expresividad, prestando poca atención a su tratabilidad. La tendencia generalizada ha sido la de ver un lenguaje de especificación como una notación matemática general y desarrollar herramientas de análisis como una idea adicional. Los resultados han sido muy pobres en términos de su impacto en la industria, ya que la generalidad se obtiene a expensas de la capacidad de análisis y de la adecuación a las aplicaciones más comunes.
  • Parcialidad en el modelado. Debido a que la formalización completa de las propiedades de un sistema grande es impracticable, la presunción ingenua de que la formalización es útil en sí misma debe abandonarse y centrarse en los detalles que merecen el coste de la formalización y los riesgos que se pretende mitigar.
  • Parcialidad en el análisis. Un lenguaje suficientemente expresivo, incluso si fue diseñado para su tratamiento, no puede ser decidible, por lo que es imposible realizar un análisis completo y correcto de muchas de las propiedades de interés. La mayoría de las especificaciones contienen errores, por lo que tienen tanto (o mayor) interés las herramientas que permiten detectar errores de forma fiable, como las que permiten encontrar demostraciones de corrección para los programas.
  • Parcialidad en la composición. Para sistemas grandes, habitualmente será necesario componer varias especificaciones parciales, que deberán soportar algún análisis de consistencia. El problema de componer diferentes vistas parciales de un sistema es algo muy bien entendido a nivel de diseño y a lo que, sin embargo, se ha prestado muy poca atención en los lenguajes de especificación.

Un enfoque lightweight como éste, en comparación con el enfoque tradicional, pierde capacidad expresiva y ámbito de aplicación, pero puede resultar mucho más efectivo a la hora de resolver problemas concretos. Sin ser tan drásticos como los partidarios a ultranza del enfoque ligero, estamos convencidos de que si se concentran los esfuerzos en etapas puntuales del desarrollo de software, renunciando a definir métodos generalistas que pretendan cubrir todo el ciclo de desarrollo, el uso de técnicas formales pueden tener finalmente una gran aceptación en la industria. Del mismo modo, consideramos que, aunque el uso de formalismos es estrictamente necesario en los llamados sistemas con requisitos críticos de seguridad}, tales como el software empotrado en un sistema de control de vuelo o en una central nuclear, su aplicación a otro tipo de sistemas menos críticos (por ejemplo, la telefonía móvil, o el desarrollo de componentes de software en general) es también factible en un entorno industrial. Así, mientras que en el primer tipo de sistemas mencionado los programas han de presentar propiedades totalmente predecibles, y a ser posible demostrables, en el resto de sistemas el objetivo debe ser minimizar el funcionamiento incorrecto.

Un número significativo de grupos orientados a la investigación teórica en informática ha evolucionado hacia el estudio de técnicas que garanticen de forma factible la calidad y fiabilidad del software como se desprende de la gran cantidad de congresos internacionales centrados en estos temas (PASTE, SEFM, ASE, ...). éste es el caso de los cuatro equipos que se integran en el presente proyecto coordinado, que ven justificadas sus investigaciones previas en la oportunidad de aplicar gran parte de su experiencia a este objetivo.

Es en este contexto en el que se desarrolla la presente propuesta, aprovechando la experiencia previa de los equipos participantes en el campo de los métodos formales y con la perspectiva de una aplicación efectiva a la Ingeniería del Software.

Finalidad

Las actividades que se desea desarrollar se pueden encuadrar dentro de las siguientes áreas:

  • Descripción semántica de componentes de software.
  • Verificación y depuración de software.
  • Optimización de programas multiparadigmas.

en las que se pretende realizar diversas aportaciones utilizando el enfoque descrito.

En la primera se pretende explorar las posibilidades que ofrecen los lenguajes de especificación basados en lógica de reescritura como Maude y los lenguajes funcionales como Haskell para describir sistemas de software en los que cada elemento (subsistema o componente) puede presentar diferentes vistas complementarias. La heterogeneidad de cada una de estas vistas puede dificultar el análisis de la consistencia de las especificaciones si no se facilita algún mecanismo para unificarlas o capturarlas bajo un mismo marco lógico; gracias a su capacidad para establecer estrategias, así como a sus posibilidades reflexivas, Maude puede aportar ese marco lógico común. Para garantizar la aplicabilidad en un entorno práctico (industrial) será necesario desarrollar técnicas para analizar la terminación de programas en Maude (y Haskell), estudiar su eficiencia, proponer técnicas de optimización automática, etc. También dentro del área relativa a la descripción semántica de componentes de software, pero a nivel de diseño de componentes, el proyecto plantea la necesidad de complementar/extender los lenguajes de descripción de interfaces (IDL) en los que se basan las plataformas/modelos de componentes actuales (CCM, EJB, .NET) para mejorar las posibilidades de análisis de corrección de sistemas construidos a base de componentes. Contamos con la experiencia previa de alguno de los grupos en el uso de álgebras de procesos para describir protocolos de interacción de componentes con información que permite analizar la compatibilidad de sistemas complejos de componentes. A partir de aquí, nuestra idea es desarrollar otras técnicas (extensiones de seguridad para álgebras de procesos, modelos de coordinación, sistemas de tipos, ...) que permitan analizar otro tipo de propiedades (de seguridad, de tiempo real, ...). La finalidad es la construcción de una herramienta que soporte este tipo de análisis de forma automatizada. Dicha herramienta podría incluso generar de forma (semi-)automática adaptadores que permitiesen la composición correcta de componentes que, debido a desajustes en sus respectivos protocolos de interacción, fuesen inicialmente incompatibles. Se espera que las técnicas desarrolladas en este área aporten nuevas posibilidades en el ``comercio'' de componentes.

En la segunda área, el objetivo del proyecto es mejorar las técnicas de model checking (comprobación de modelos) y proof carrying code (código con demostración asociada) para el análisis automático de sistemas software basados en componentes. Así, por un lado, se aplicarán a este contexto las ``lecciones aprendidas" sobre model checking y, en particular, las orientadas a disminuir la complejidad del modelo analizado para resolver el problema de la explosión de estados. Siendo coherentes con las nociones de parcialidad y eficacia comentadas anteriormente, las técnicas desarrolladas en el marco del proyecto deben adaptarse a las aplicaciones que se analizan y al tipo de propiedades analizadas, y deben estar orientadas a la automatización del proceso de verificación. En este sentido, el proyecto plantea la adaptación de notaciones, algoritmos y herramientas basadas en model checking para el análisis de propiedades funcionales (restricciones temporales de la interacción entre distintas componentes, o entre una componente y el entorno) y extra-funcionales (propiedades de tiempo real y de prestaciones). En particular, el trabajo se enfocará al análisis de lenguajes de programación y a aplicaciones específicas. En todos los casos, para controlar la complejidad de la verificación habrá que considerar técnicas de abstracción y de razonamiento composicional, especialmente adecuadas para software basado en componentes. Un enfoque alternativo para la verificación de código es el conocido como proof carrying code. En general, cuando se plantea la posibilidad de validar ciertas propiedades sobre una componente de software, no se tiene en cuenta la forma de garantizar a los posibles usuarios/clientes de dicha componente que esa ``certificación'' se ha realizado. Desde el punto de vista de la eficiencia, no es aceptable que el cliente tenga que volver a validar (posiblemente en tiempo de ejecución) la propiedad ya verificada por el proveedor del código. Para evitar esto, existen técnicas que permiten adjuntar al código (binario) la ``demostración'' de la validación realizada. En el proyecto se plantea la aplicación de estas técnicas a entornos de programación declarativos (en particular, funcionales).

Como ha podido observarse, muchos de los objetivos del proyecto pueden relacionarse con la explotación de las posibilidades de los lenguajes declarativos multiparadigma (lógica, funciones, concurrencia, restricciones, etc.). Por ello, la propuesta, dentro de la tercera área, también se interesa por conseguir que la eficiencia de estos lenguajes sea comparable a la de los lenguajes imperativos (tal y como lo han conseguido lenguajes como Haskell o Prolog). Este es un requisito indispensable para hacer posible su uso en entornos industriales para el desarrollo de aplicaciones. Y en relación con las aplicaciones, y manteniendo el enfoque ágil que propugna la parcialidad en el modelado, el proyecto también hace énfasis en dominios de aplicación específicas donde los lenguajes multiparadigma pueden resultar eficaces. El análisis de datos ha experimentado un avance y popularización muy significativos en la última década, gracias a la incorporación de técnicas de aprendizaje automático. La mayoría de los métodos y algoritmos de aprendizaje propuestos trabajan con datos en formato atributo-valor y, por lo tanto, son capaces de encontrar patrones en fuentes de datos cuya información se almacena en una sola tabla. Sin embargo, las aplicaciones reales o usan datos organizados en diversas tablas o usan datos con una estructura compleja, como en las aplicaciones de bioinformática. éstas son las razones por las que el uso de técnicas declarativas basadas en formalismos lógicos más potentes se está perfilando como una solución apropiada.