Objetivos del Proyecto

Este proyecto sigue dos líneas de investigación principales. Por un lado, estamos interesados en el modelado y verificación formal de sistemas discretos enriquecidos con componentes continuas y aspectos de incertidumbre. Esto enmarca la propuesta dentro del área de modelado y verificación de sistemas híbridos y probabilísticos. Por otro lado, el proyecto aborda el desarrollo de técnicas de síntesis y optimización, que son de suma importancia en las áreas de diseño de controladores software, y de adaptadores de servicios. Como técnica básica para resolver ambos problemas, en el proyecto se utilizará el model checking. El equipo de trabajo tiene mucha experiencia en esta técnica formal, por lo que parece la más adecuada para afrontar nuevos retos.

Por otro lado, está claro que las técnicas formales sólo tienen una verdadera aplicación práctica si van acompañadas de herramientas que soportan las propuestas teóricas. En este sentido, se propone la construcción de prototipos que incorporen estas propuestas.

Finalmente, el proyecto propone el modelado, verificación y/o síntesis de aplicaciones de tamaño medio, y de una aplicación de gran entidad a desarrollar por la empresa que colabora en el proyecto motriz. Esta aplicación culmina de manera coherente las propuestas tecnológicas realizadas.

A continuación se incluye una descripción de los objetivos concretos que se persiguen en este proyecto. Con idea de que se puedan establecer conexiones con la finalidad del proyecto, los objetivos se enumeran atendiendo a las cuatro tareas en las que se desarrollarán las actividades:

  1. Avances en model checking de sistemas híbridos

    Se persigue la definición de un lenguaje de modelado formal que incluya aspectos continuos, además de los discretos, y para el que se desarrollará una herramienta de verificación automática a partir de las existentes. El lenguaje y la herramienta deberán ser aplicables en problemas reales en sistemas empotrados de naturaleza híbrida, como el caso de sistemas de control ferroviario.
  2. Avances en verificación y síntesis de sistemas probabilísticos y su aplicación a protocolos de comunicaciones

    Se pretende obtener una metodología para la verificación y optimización de sistemas parcialmente probabilísticos, como los modelos de los protocolos de comunicaciones. Para ello, se integrarán las técnicas de model checking con los simuladores de red tradicionales como ns-2 y OPNET. La metodología y del conjunto de herramientas resultante debe ser aplicable a protocolos reales, como los que soportan el servicio de videostreaming en comunicaciones móviles.
  3. Avances en generación automática de adaptadores en tiempo de ejecución

    Se persigue desarrollar un marco para la generación automática de adaptadores de servicios basado en el uso de técnicas formales, explorando sobre todo el uso de model checking como técnica para la síntesis de adaptadores a partir del modelado formal de los interfaces requeridos y ofrecidos por los servicios existentes y por otras informaciones de contexto. La metodología, los lenguajes de especificación y las herramientas resultantes se utilizarán para la adaptación en servicios de gran actualidad, como el acceso a las redes sociales desde dispositivos móviles.
  4. Demostración de la aplicabilidad de los resultados en una aplicación compleja con impacto industrial en el campo de las comunicaciones inalámbricas

    Se plantea aplicar el resto de resultados del proyecto en un dominio de aplicación en el que estén presentes los comportamientos híbridos y probabilísticos y que requiera del modelado, verificación y optimización. Concretamente, se pretende extender la certificación en redes UMTS y LTE para abarcar la certificación de los nuevos servicios como la voz IP sobre conmutación de paquetes. En este contexto, hay que abordar el modelado y verificación de aspectos continuos como el nivel de señal o el consumo de energía, así como aspectos probabilísticos relacionados con la pérdida de paquetes, o con el tipo de tráfico generado. Se hará un uso real de la integración de model checking y simuladores de protocolos para la síntesis automática de configuraciones óptimas de las pilas de protocolos, adecuadas a la calidad de servicio que se demanda. El resultado debe ser la extensión de infraestructuras de certificación de protocolos LTE existentes para contemplar medidas de QoS en servicios emergentes.

Proyecto financiado por

Documento de la Propuesta