Máster Oficial en Métodos Formales en Ingeniería Informática

La creación del software se enfrenta actualmente a grandes desafíos derivados del papel omnipresente del mismo en la sociedad actual: dependemos de programas que controlan dispositivos, vehículos, transacciones bancarias, el mercado de valores, aparatos médicos, etc. Aparte de los casos de pérdida de vidas humanas por fallos en el software, estos causan con frecuencia enormes trastornos en las vidas de millones de personas. Hoy por hoy, el único método conocido para asegurar la corrección del software pasa por utilizar los llamados métodos formales, que se caracterizan a grandes rasgos por la modelización matemática del software, y de los procesos que este realiza, para conseguir demostrar que se cumplen los requisitos deseados.

Esta dependencia de la sociedad actual del software y la complejidad del mismo han hecho que este enfoque está recibiendo atención renovada en los últimos tiempos. Por ejemplo, Amazon usa bases distribuidas por todo el planeta que realizan millones de transacciones por segundo que deben ser coherentes, para lo cual se emplean algoritmos distribuidos extremadamente complejos. Los métodos tradicionales de desarrollo y testing no son capaces de encontrar errores sutiles en ellos, que causarían la pérdida de datos y el consiguiente perjuicio económico. Estos errores solo se manifiestan en una pequeña fracción de los posibles estados. Pero, dada la magnitud del software, sucederían con preocupante frecuencia de no encontrarse y resolverse, lo cual Amazon hizo mediante el uso de técnicas de verificación formal. Otro ejemplo revelador es el desarrollo del software de control de la línea 14 de metro de Paris, realizada íntegramente mediante métodos formales. Tras la generación del código, las pruebas durante la simulación y las realizadas en el entorno real no revelaron ningún error en las más de 80.000 líneasde código generadas automáticamente.

1. Fundamentos

2. Métodos
2.1 Análisis de corrección de sistemas
2.2 Diseño y construcción rigurosos de software
2.3 Técnicas especializadas
2.4 Prácticas

3.1. Trabajo de fin de Máster