Innovating Works

PID2021-122830OB-C43

Financiado
METODOS FORMALES ESCALABLES PARA APLICACIONES EN ENTORNOS REALES
DADA LA UBICUIDAD DE LOS SISTEMAS INFORMATICOS EN APLICACIONES CUYA SEGURIDAD ES CRITICA, ES CADA VEZ MAS IMPORTANTE PARA LA SOCIEDAD ASEGURAR QUE DICHOS SISTEMAS SE COMPORTAN CORRECTAMENTE. EL PROYECTO SFERA APLICA METODOS FORMAL... DADA LA UBICUIDAD DE LOS SISTEMAS INFORMATICOS EN APLICACIONES CUYA SEGURIDAD ES CRITICA, ES CADA VEZ MAS IMPORTANTE PARA LA SOCIEDAD ASEGURAR QUE DICHOS SISTEMAS SE COMPORTAN CORRECTAMENTE. EL PROYECTO SFERA APLICA METODOS FORMALES PARA GARANTIZAR, A TRAVES DE RAZONAMIENTOS FORMALES, LA CORRECTA EJECUCION DE LOS SISTEMAS INFORMATICOS, CENTRANDOSE ASI EN EL AREA DE PRIORIDAD ``MUNDO DIGITAL, INDUSTRIA, ESPACIO Y DEFENSA'' Y, EN PARTICULAR, EN SU LINEA ESTRATEGICA ``MODELIZACION Y ANALISIS MATEMATICO Y NUEVAS SOLUCIONES MATEMATICAS PARA CIENCIA Y TECNOLOGIA''. UNA VENTAJA DE LOS METODOS FORMALES ES QUE SON CAPACES DE PROPORCIONAR GARANTIAS MATEMATICAS SOBRE LA PROTECCION Y SEGURIDAD DE LOS METODOS ANALIZADOS MODULO LA PRECISION DE LOS METODOS FORMALES UTILIZADOS, Y TAMBIEN DE LA CORRECCION DE LOS RAZONAMIENTOS USADOS EN LA IMPLEMENTACION. SIN EMBARGO, DEPENDIENDO DE LA PRECISION Y LA ESCALABILIDAD DE LAS TECNICAS UTILIZADAS, NO SIEMPRE ES POSIBLE OBTENER UN RESULTADO A PARTIR DE ELLAS. ESTE ES PRECISAMENTE EL NUCLEO PRINCIPAL DEL PROYECTO SFERA: PASAR DE UN AMBITO GENERAL --PERO NO SIEMPRE PRECISO Y EFICIENTE-- A APROXIMACIONES MAS PRECISAS Y ESCALABLES. ACTUALMENTE, Y SIN MENOSPRECIAR LOS ESFUERZOS REALIZADOS (INCLUYENDO NUESTROS PROYECTOS PREVIOS), LA APLICACION DE METODOS FORMALES A SISTEMAS DEL MUNDO REAL Y DE TAMAÑO GRANDE HA ESTADO LIMITADO A POCOS CASOS Y EN DOMINIOS ESPECIFICOS.EL PROYECTO SFERA ESTA ENFOCADO A INVESTIGAR Y MEJORAR LA ESCALABILIDAD Y PRECISION, DENTRO DE SUS CUATRO OBJETIVOS CIENTIFICOS, Y ASI LOGRAR AVANCES SIGNIFICATIVOS DENTRO DE LOS METODOS FORMALES, CON ESPECIAL ATENCION EN LA APLICABILIDAD DE LAS TECNICAS DESARROLLADAS PARA ASEGURAR LA FIABILIDAD Y EFICIENCIA EN APLICACIONES A GRAN ESCALA. SE UTILIZARA VERIFICACION, TESTEO, ANALISIS Y OPTIMIZACION 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 PROPOSITOS, EL USO DE RESOLUTORES PARA PROBLEMAS RELACIONADOS CON SAT SERA ESENCIAL. ESPERAMOS CONSEGUIR LAS SIGUIENTES CONTRIBUCIONES DENTRO DE NUESTROS CUATRO OBJETIVOS: (1) DESARROLLAR TECNICAS ESCALABLES Y HERRAMIENTAS PARA RESOLVER PROBLEMAS QUE SEAN RELEVANTES PARA LA INDUSTRIA, (2) AVANZAR EN LA SINTESIS DE PROPIEDADES COMPLEJAS, QUE SURGEN EN EL CONTEXTO DE LAS APLICACIONES REALES, (3) MEJORAR LAS TECNICAS DE METODOS FORMALES PARA SU MEJOR ESCALABILIDAD Y (4) DESARROLLAR TECNICAS E INSTRUMENTOS PARA MEDIDAS Y SUPERVISION EN INTELIGENCIA ARTIFICIAL, APRENDIZAJE AUTOMATICO Y TESTEO.SFERA ES UN PROYECTO COORDINADO CON CUATRO GRUPOS DE INVESTIGACION 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 AREA DE LOS LENGUAJES DE PROGRAMACION, A NIVEL SEMANTICO Y DE IMPLEMENTACION. UCM TIENE MAS EXPERIENCIA EN LA VERIFICACION, TESTEO Y TECNICAS DE ANALISIS DE PROGRAMAS. UPC INVESTIGA EN LA TEORIA DE HERRAMIENTAS DEDUCTIVAS Y EN APLICACIONES INDUSTRIALES. UPM TIENE UNA EXPERIENCIA RELEVANTE EN LA CERTIFICACION, ANALISIS INCREMENTAL, SISTEMAS ESCALABLES, Y EN LA TRANSFERENCIA TECNOLOGICA 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. AZONAMIENTO FORMAL\BIOINFORMATICA\SEGURIDAD\CONTRATOS INTELIGENTES\APRENDIZAJE\TRANSFORMACION\TESTING\VERIFICACION\ANALISIS ESTATICO\RESOLUCION DE RESTRICCIONES ver más
01/01/2021
UPC
121K€
Perfil tecnológico estimado

Línea de financiación: concedida

El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto el día 2021-01-01
Presupuesto El presupuesto total del proyecto asciende a 121K€
Líder del proyecto
Universidad Politécnica de Cataluña No se ha especificado una descripción o un objeto social para esta compañía.
Total investigadores 9