Grupos de inestigación de la UB

PROMETHEUSS GRUP

QUIÉNES SOMOS

Equipo

Dr. Joost J. Joosten. Director. Especialista en Teoría de la Demostración y Lógica Modal. •
Dr. David Fernández Duque. Especialista en aplicaciones de la Lógica Modal a la topología y a la Teoría de la Demostración. Herramientas computacionales para la representación y el razonamiento automático de reglamentos. •
Aleix Solé Sánchez. Ontologías y métodos formales. Construcción de la arquitectura, formalización y transformación de datos. •
Eric Sancho Adamson. Métodos formales y análisis de datos. Evaluación, estructuración y formalización de datos complejos. •
Ana de Almeida Gabriel Vieira Borges, Mireia González Bedmar y Juan José Conejero Rodríguez. Software formalmente verificado, y formalización de textos legales. • Daniel Sousa. Desarrollo de software formalmente verificado. •
Gina García Tarrach. Desarrollo de software formalmente verificado y la evaluación y estructuración de datos.

CONTACTO

Fundació Bosch i Gimpera
Innovation and Transfer Office
Parc Científic de Barcelona.
C/Baldiri i Reixac 08028,
Barcelona (Spain)
+34934039796
fbenlliure@fbg.ub.edu

Mientras la dependencia de las tecnologías informáticas aumentan, la cuestión compleja de los errores de software (o bugs) no está resuelta. A su vez, dentro del software tradicional, no existe un modo último de comprobar el lazo entre las especificaciones y el código final del sistema. FV (formal verification) asegura que matemáticamente la ejecución de nuestros softwares es literalmente la que expresa sus especificaciones, así como la total ausencia de bugs. Por ejemplo existen protocolos estandarizados para las comunicaciones financieras como el FIX (siglas en inglés del protocolo de intercambio de información financiera, una norma internacional para la negociación electrónica), con el propósito de regular estos intercambios y hacerlos seguros. Los clientes que quieren adaptarse al sistema están atrapados por cientos de páginas de reglas y divulgaciones escritas en prosa legal. Se ven obligados a contratar a personas para que entiendan esos ensayos y descubran cómo asegurarse de que sus sistemas sean consistentes y cumplan con las reglas y divulgaciones del FIX. Pero esa información puede especificarse en un formato matemáticamente preciso, lo que permitiría a los clientes aprovecharse de la innovadora herramienta científica de FV para garantizar que sus sistemas cumplan plenamente todas las complejidades de la negociación.

QUÉ HACEMOS

Servicios

Al proporcionar a los clientes un sistema verificado a partir de especificaciones precisas, los homologadores pueden monetizar parte del ahorro de costos. Sin mencionar que la FV permitirán que los clientes tengan softwares más seguros. Esto es un win / win para todos. La administración pretende establecer sistemas que permitan la verificación de los algoritmos complejos para todos aquellos ámbitos más sensibles, como los relativos a transporte de personas, armas, finanzas…

Los sistemas de seguridad críticos clásicos (por ejemplo, el algoritmo autopilot de un avión comercial) pueden y deben testear un número elevado de escenarios. Con FV podemos analizar todos los comportamientos posibles de un algoritmo. El método de la verificación formal construye el algoritmo mediante herramientas matemáticas a partir de las especificaciones: el uso de dichas herramientas matemáticas excluye la posibilidad de comportamientos inesperados. Es por esto que se le llama software verificado de “fallo cero”.

INVESTIGACIÓN

Proyectos de investigación

Cuando se trata de razonar exhaustivamente sobre el comportamiento de algoritmos complejos, la única solución viable es la verificación formal, el uso de los avances profundos en lógica matemática para razonar automáticamente sobre algoritmos y probar las propiedades de los programas. El campo de verificación formal (FV) aúna las matemáticas, la informática y la inteligencia artificial, y está dedicado a analizar el comportamiento de los algoritmos complejos para asegurarse de que estén diseñados e implementados correctamente. De la misma manera que un alcoholímetro transforma el problema cualitativo de argumentar que alguien está intoxicado mediante los conocimientos del dominio científico de la química, FV transformará el cumplimiento normativo en torno a los algoritmos en el dominio de las matemáticas. Después de todo, los algoritmos son objetos matemáticos, las matemáticas por lo tanto deben usarse para describirlas y analizarlas.

REFERENCIAS

Comparte esta entrada:

Utilitzem cookies de tercers amb finalitats tècniques i analítiques. Si continua navegant vol dir que accepta la nostra política de cookies. Més informació,plugin cookies política de cookies.

ACEPTAR
Aviso de cookies