Hola,
¿eres nuevo aquí?

Regístrate gratis y conecta tu empresa con financiación pública, partners y proyectos.

Tengo cuenta

Regístrate

Ver video

PID2021-122830OA-C44

Financiado

METODOS FORMALES ESCALABLES PARA APLICACIONES 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... ver más

01/01/2021

UPM

68K€

Presupuesto del proyecto: 68K€

Líder del proyecto

UNIVERSIDAD POLITÉCNICA DE MADRID No se ha especificado una descripción o un objeto social para esta compañía.

Total investigadores 3944

Financiación concedida El organismo AGENCIA ESTATAL DE INVESTIGACIÓN notifico la concesión del proyecto el día 2021-01-01 No tenemos la información de la convocatoria

0% 100%

Participantes

UPM

Lider

Conecta tu I+D

¿Tienes un proyecto y buscas un partner? Gracias a nuestro motor inteligente podemos recomendarte los mejores socios y ponerte en contacto con ellos. Te lo explicamos en este video

Proyectos interesantes

CHORDS Compositional Higher-Order Reasoning about Distributed Syste... 2M€ Cerrado

PID2021-122830OB-C41 METODOS FORMALES ESCALABLES PARA APLICACIONES EN ENTORNOS RE... 178K€ Cerrado

AutoProbe Automated Probabilistic Black Box Verification 2M€ Cerrado

TIN2015-71819-P TECNOLOGIAS RIGUROSAS PARA EL ANALISIS Y VERIFICACION DE SOF... 108K€ Cerrado

TIN2010-20639 VERIFICACION PARAMETRIZADA DE SISTEMAS INFORMATICOS 44K€ Cerrado

TIN2009-14599-C03-03 DESARROLLO DE SOFTWARE DE ALTA CALIDAD, FIABLE, DISTRIBUIDO... 159K€ Cerrado

Líder del proyecto

UNIVERSIDAD POLITÉCNICA DE MADRID No se ha especificado una descripción o un objeto social para esta compañía.

Total investigadores 3944

Presupuesto del proyecto 68K€

Descripción del proyecto 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

Conecta tu I+D

Entra hoy

¿Olvidé mi contraseña?

Financiación

Empresas

CTIs/Universidades

Proyectos

Investigadores