Resumen
Dada la ubicuidad de los sistemas informáticos en aplicaciones cuya seguridad es crítica, es cada vez más importante para la sociedad
asegurar que dichos sistemas se comportan correctamente. El proyecto SFERA aplica métodos formales para garantizar, a través de
razonamientos formales, la correcta ejecución de los sistemas informáticos, centrándose así en el área de prioridad "mundo digital,
industria, espacio y defensa'' y, en particular, en su línea estratégica "modelización y análisis matemático y nuevas soluciones
matemáticas para ciencia y tecnología''. Una ventaja de los métodos formales es que son capaces de proporcionar garantías matemáticas
sobre la protección y seguridad de los métodos analizados módulo la precisión de los métodos formales utilizados, y también de la
corrección de los razonamientos usados en la implementación. Sin embargo, dependiendo de la precisión y la escalabilidad de las
técnicas utilizadas, no siempre es posible obtener un resultado a partir de ellas. Este es precisamente el núcleo principal del proyecto
SFERA: pasar de un ámbito general --pero no siempre preciso y eficiente-- a aproximaciones más precisas y escalables. Actualmente, y
sin menospreciar los esfuerzos realizados (incluyendo nuestros proyectos previos), la aplicación de métodos formales a sistemas del
mundo real y de tamaño grande ha estado limitado a pocos casos y en dominios específicos.
El proyecto SFERA está enfocado a investigar y mejorar la escalabilidad y precisión, dentro de sus cuatro objetivos científicos, y así lograr
avances significativos dentro de los métodos formales, con especial atención en la aplicabilidad de las técnicas desarrolladas para
asegurar la fiabilidad y eficiencia en aplicaciones a gran escala. Se utilizará verificación, testeo, análisis y optimización sobre un amplio
rango de sistemas, desde "smart contracts" que se ejecutan sobre el "blockchain", hasta protocolos de seguridad y aplicaciones dirigidas
por datos. Para algunos de estos propósitos, el uso de resolutores para problemas relacionados con SAT será esencial. Esperamos
conseguir las siguientes contribuciones dentro de nuestros cuatro objetivos: (1) desarrollar técnicas escalables y herramientas para
resolver problemas que sean relevantes para la industria, (2) avanzar en la síntesis de propiedades complejas, que surgen en el contexto
de las aplicaciones reales, (3) mejorar las técnicas de métodos formales para su mejor escalabilidad y (4) desarrollar técnicas e
instrumentos para medidas y supervisión en inteligencia artificial, aprendizaje automático y testeo.
SFERA es un proyecto coordinado con cuatro grupos de investigación de UCM, UPV, UPC y UPM. Los conocimientos complementarios
de estos grupos son fundamentales para conseguir los objetivos del proyecto: UPV tiene amplia experiencia en el área de los lenguajes
de programación, a nivel semántico y de implementación. UCM tiene más experiencia en la verificación, testeo y técnicas de análisis de
programas. UPC investiga en la teoría de herramientas deductivas y en aplicaciones industriales. UPM tiene una experiencia relevante en
la certificación, análisis incremental, sistemas escalables, y en la transferencia tecnológica a la industria. Los grupos han colaborado con
investigadores internacionales de reconocido prestigio y en la actualidad trabajan de forma activa con empresas en temas muy
relacionados con el proyecto SFERA.
