Diseño y Análisis Formal de Sistemas de Software
(Formal Analysis and Design of Software Systems, FADoSS)

Grupo de investigación validado por la UCM con número 910398.

Director

Narciso Martí Oliet
Departamento de Sistemas Informáticos y Computación
Facultad de Informática
Universidad Complutense de Madrid
narciso@ucm.es
+34 91 394 7557

Descripción

El grupo de investigación sobre Diseño y Análisis Formal de Sistemas de Software (Formal Analysis and Design of Software Systems, FADoSS) en el Departamento de Sistemas Informáticos y Computación de la UCM es el resultado de la evolución de los antiguos grupos de métodos formales para la concurrencia y de programación funcional paralela. En 2005 fue reconocido como grupo oficial de investigación por la UCM y en la actualidad consta de 16 doctores y 4 estudiantes de doctorado, siendo su director Narciso Martí.

La actividad principal del grupo FADoSS se centra en el estudio y desarrollo de técnicas rigurosas que garanticen la corrección del diseño de los sistemas de software. También se persigue la aplicación de los desarrollos teóricos en sistemas concretos de programación (Edén), especificación (Maude) y modelado, análisis y generación de código (ActionGUI).

La investigación del grupo ha sido financiada ininterrumpidamente desde su creación mediante proyectos nacionales y regionales, siendo los más recientes los proyectos PROMESAS de la Comunidad de Madrid, DESAFIOS del Ministerio de Educación y Ciencia, DESAFIOS10 del Ministerio de Ciencia e Innovación y PROMETIDOS-CM de la Comunidad de Madrid, todos ellos realizados en diferentes formas de colaboración con los grupos GPD del mismo departamento, CLIP y Babel de la Universidad Politécnica de Madrid, e IMDEA Software. Además, miembros del grupo FADoSS participan en la Red de Excelencia Europea NESSoS, financiada por el 7º Programa Marco. El grupo FADoSS también mantiene relaciones de colaboración con empresas líderes en su sector, como SIEMENS y Deimos Space, y ha realizado proyectos de I+D para empresas como INDRA y EADS.

Los resultados de la investigación realizada por el grupo FADoSS han sido publicados en revistas y actas de numerosos congresos internacionales, siendo citados frecuentemente por otros investigadores del área. Los miembros de FADoSS también participan habitualmente en comités de programa de congresos internacionales y han organizado algunos prestigiosos congresos internacionales como POPL 2010 en Madrid, ESSoS 2011 en Madrid, TFP 2011 en Madrid y WADT 2012 en Salamanca.

El grupo tiene amplios contactos y proyectos conjuntos con investigadores externos, tanto en España como en el extranjero. Además de los cuatro proyectos conjuntos mencionados antes, en la acción complementaria Red Maude también participaron investigadores de seis universidades españolas. El grupo FADoSS también mantiene una estrecha relación con el instituto de investigación IMDEA Software de la Comunidad de Madrid. Entre las colaboraciones internacionales, destacan las establecidas con los grupos de investigación de los profesores José Meseguer en la Universidad de Illinois en Urbana-Champaign (Estados Unidos), David Basin en el ETH Zürich (Suiza), Carolyn Talcott en SRI International (Estados Unidos), Rita Loogen en la Philipps-Universität Marburg (Alemania), y Luca Aceto y Anna Ingólfsdóttir en la Universidad de Reikiavik (Islandia).

Los miembros del grupo FADoSS participan en el programa de posgrado de la Facultad de Informática impartiendo asignaturas sobre especificación y validación de software, sobre modelos de sistemas concurrentes y distribuidos, y sobre análisis y transformación de programas, y dirigiendo trabajos de fin de máster. Asimismo, han dirigido varias tesis doctorales en el programa de doctorado de Ingeniería Informática. Finalmente, han participado a nivel internacional en la impartición de cursos en escuelas de verano en diversos países.


Líneas de investigación

Técnicas de especificación y verificación de sistemas.
Semántica de lenguajes de especificación y programación.
Análisis estático de programas y sistemas de tipos.
Diseño e implementación de lenguajes de programación funcional paralela.
Estudio y aplicaciones informáticas de la lógica de reescritura.
Diseño e implementación del lenguaje Maude basado en la lógica de reescritura.
Modelos formales para la movilidad y la seguridad.
Desarrollo de sistemas seguros a partir de modelos.