Subproyecto 1: Universidad de Málaga

Módulo M-1.1: La integración de múltiples perspectivas en el desarrollo de software
    La construcción de una descripción o un modelo complejo involucra a muchos participantes, los cuales tienen perspectivas o puntos de vista distintos del sistema que tratan de describir o modelar. Estas perspectivas o puntos de vista son descripciones parciales o incompletas que surgen de las diferentes responsabilidades asignadas a cada uno de estos participantes. Así, cada una de estas ``vistas'' es un modelo que permite a uno de los participantes en el desarrollo de un sistema de software enfrentarse a cuestiones concretas sobre el sistema en desarrollo. Es habitual que haya múltiples participantes en el desarrollo de cualquier sistema, o que se encuentre apropiado el utilizar diferentes modelos o formalismos para modelar distintos aspectos del mismo sistema, y por tanto es útil el uso de múltiples puntos de vista, de forma que cada uno de ellos pueda trabajar de forma independiente.

    Existe sin embargo una cierta tensión en la práctica entre la expresividad de múltiples vistas y la eficiencia en establecer y mantener la consistencia y la coherencia entre dichos puntos de vista. Las múltiples vistas tienen una larga historia en la ingeniería del software, siendo necesario remontarse al menos hasta los años 70 para encontrar sus inicios, en trabajos como el Análisis Estructurado de Ross, y aunque la primera cuestión está ampliamente aceptada, y las vistas se ven como constructores esenciales por ejemplo en ingeniería de requisitos o para expresar descripciones arquitectónicas, el garantizar la consistencia o integración de las vistas es un área de investigación muy activo.

Módulo M-1.2: Coordinación de componentes de software

    Las actuales plataformas orientadas a componentes (CORBA, EJB, .NET) sólo explotan la interoperabilidad del software al nivel de la signatura de servicios. Las interfaces descritas mediante IDL permiten superar desajustes a nivel de signatura (pues proporcionan información sobre el nombre de los métodos, el tipo y número de sus argumentos o el tipo del resultado), sin embargo, no existen garantías de que dos componentes vayan a interactuar convenientemente, ya que pueden darse desajustes debidos a diferencias en el comportamiento de la interacción de las componentes involucradas. Estas limitaciones de los IDL, entre otras, ha hecho que se estén coordinando esfuerzos para extender (o complementar) estos lenguajes con información adicional, susceptible de ser analizada de distintas formas. Una forma natural de enriquecer la descripción de las interfaces de lss componentes mediante protocolos de interacción la ofrecen las álgebras de procesos y determinados modelos de coordinación como Linda. Esta información sobre el comportamiento de una componente podría ser utilizada para determinar ciertas propiedades de la misma. En particular, para conocer las posibilidades de composición segura (sin interbloqueo) con otras componentes. No obstante, la comprobación de gran parte de esas propiedades es costosa si se utilizan métodos habituales de descripción de comportamiento concurrente, como son las álgebras de procesos. Por ello, en este módulo proponemos explorar otras alternativas. En particular, los modelos de coordinación y los sistemas de tipos para sesiones introducidos en prometen ser muy adecuados para este uso. Asimismo, el desajuste en los protocolos de interacción de dos componentes no debería resolverse exclusivamente con una notificación sobre este hecho, sino que, en el caso de que sea posible, proponer algún tipo de adaptación que permita acomodar sus respectivos protocolos de comunicación. Este aspecto será estudiado en una tarea dedicada a la adaptación automática de software basado en componentes. En cada una de las tres tareas que se proponen inicialmente existe la posibilidad de construir herramientas que soporten la metodología de descripción, análisis y adaptación de componentes de forma automática. Esta es la razón de incluir una cuarta tarea para desarrollar un entorno integrado que soporte este tipo de posibilidades. Con objeto de evaluar las posibilidades prácticas de aplicación de los resultados de este proyecto, se usará un dominio de apicación específico, como es el de la telefonía. Asimismo, los estudios se aplicarán en el contexto de los servicios web (web services donde este tipo de extensiones pueden ser de gran utilidad. De hecho, existen trabajos en este sentido sobre lenguajes de descripción de servicios web (WSDL) que podrían verse beneficiados con las capacidades de anàlisis que en este módulo y en el módulo\ref{UMA-M3} se desarroillarán.

Módulo M-1.3: Análisis de propiedades de sistemas basados en componentes

    El objetivo de este módulo es la extensión e integración de las técnicas de model checking, muy maduras en algunos ámbitos, al contexto de análisis de propiedades de software basado en componentes. Esta extensión e integración puede afrontarse desde distintas perspectivas, aunque siempre con el objetivo de que la verificación sea completamente automatizable. Por ejemplo, con respecto a los lenguajes de modelado, es necesario explorar notaciones más expresivas, que extiendan formalismos existentes que son adecuados, por ejemplo, para analizar propiedades funcionales, con otros aspectos complementarios, como puede ser la incorporación del tiempo para analizar prestaciones. Existe, sin embargo, un enfoque alternativo a la extensión de formalismos, que consiste en la integración de herramientas, que soportan lenguajes de modelado y especificación diferentes orientados a un tipo de propiedades específicas. Finalmente, una última posibilidad es afrontar el análisis de propiedades de sistemas finales (descritos en un lenguaje de programación concreto). En este caso, para manejar la complejidad del código analizado, la verificación se centrará en sistemas construidos con interfaces bien definidos para un dominio de aplicación específico, como puede ser la telefonía móvil. En cada una de las alternativas descritas será necesario extender las técnicas de abstracción para resolver el problema de la explosión de estados inherente a la aplicación del model checking. La abstracción no es sólo aplicable en el contexto del análisis de propiedades funcionales y extra-funcionales, sino que también es adecuada, en combinación con métodos de razonamiento composicional, para analizar la consistencia entre distintos puntos de vista de una componente, análisis que es imprescindible cuando se añaden nuevas funcionalidades a las componentes.