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 integración de los antiguos grupos de métodos formales para la concurrencia y de programación funcional paralela, y posteriormente del grupo de programación declarativa, además del crecimiento natural del grupo a lo largo de sus más de veinte años de historia. En 2005 fue reconocido como grupo oficial de investigación por la UCM y en la actualidad consta de 26 doctores, 3 estudiantes de doctorado y 6 colaboradores externos, siendo sus directores Fernando Rubio y Adrián Riesco.
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, especificación y modelado, como Maude.
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 BLOQUES de la Comunidad de Madrid y ProCode del Ministerio de Ciencia e Innovación, casi todos ellos realizados en diferentes formas de colaboración con los grupos CLIP y Babel de la Universidad Politécnica de Madrid, e IMDEA Software. Además, miembros del grupo han participado en algunos proyectos europeos. El grupo FADoSS también mantiene relaciones de colaboración y ha realizado proyectos de I+D con empresas.
Los resultados de la investigación realizada por el grupo FADoSS se publican en revistas y actas de numerosos congresos de ámbito internacional, siendo citados frecuentemente por otros investigadores del área. Los miembros de FADoSS también participan habitualmente en comités de programa de estos congresos y han organizado algunos de ellos de reconocido prestigio como POPL 2010, MPC 2012, PPDP 2013, LOPSTR 2013, CONCUR 2015, ISR 2021, ICFEM 2022.
El grupo tiene amplios contactos y proyectos conjuntos con investigadores externos, tanto en España como en el extranjero. Además de los 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), Kazuhiro Ogata en JAIST (Japón), Carolyn Talcott en SRI International (Estados Unidos), Rita Loogen en la Philipps-Universität Marburg (Alemania), Luca Aceto y Anna Ingólfsdóttir en la Universidad de Reikiavik (Islandia), Daniel Gaina en la Universidad de Kyushu (Japón) y Marco Gavanelli en la Universidad de Ferrara (Italia).
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, entre otros temas de métodos formales, 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.
- Estudio y aplicaciones informáticas de la lógica de reescritura.
- Diseño e implementación del lenguaje Maude.
- Modelos formales para la movilidad y la seguridad.
- Demostración semi-automática de teoremas.
- Complejidad computacional de problemas y métodos heurísticos de resolución.
- Estudio de propiedades lógicas de los sistemas informáticos.
- Testing y modelado de sistemas distribuidos.