Métodos formales

En los sistemas de software, los errores pueden tener consecuencias catastróficas, sobre todo en los sistemas críticos para la seguridad como los programas médicos o aeroespaciales. Aunque las verificaciones y revisiones de código pueden reducir la tasa de errores, en algunos casos es necesario disponer de un nivel de seguridad más alto. Con este objetivo, los métodos formales se integran en una categoría de técnicas que analizan una descripción matemática del sistema para garantizar su exactitud.

Algunas de las técnicas que se utilizan para la verificación formal del software son la comprobación de modelos, la demostración de teoremas y el análisis estático. Un problema que tienen en común todos estos métodos es la gran complejidad computacional, que puede limitar su aplicabilidad en ejemplos del mundo real. Esta línea de investigación tendrá en cuenta los enfoques pragmáticos para garantizar la calidad de los sistemas de software a escala industrial y explorará temas clave como la usabilidad, la eficiencia y la aplicabilidad.

Ingeniería dirigida por modelos

El desarrollo dirigido por modelos es un paradigma que promueve el uso de modelos de software en todas los trabajos de diseño de programas (ingeniería directa, ingeniería inversa, interoperabilidad...), como se hace habitualmente en todas las demás disciplinas de ingeniería. Por ejemplo, intenta reducir los costes de desarrollo centrándose en la creación de modelos de software (especificados en UML o por medio de lenguajes específicos del dominio) más que en el código, y una vez dichos modelos se han validado, se basa en herramientas de generación de código para generar automáticamente la implementación final de estos modelos.

En esta línea de investigación exploramos técnicas y herramientas para sustentar todos los aspectos de la ingeniería dirigida por modelos, incluyendo la manipulación de modelos muy grandes, modelos heterogéneos, modelado colaborativo y descubrimiento de modelos (de API en código fuente).

Analítica de software

La analítica de software es el estudio de todos los datos relacionados con los programas y sus procesos de ingeniería con el fin de entender mejor cómo se construye el software. El objetivo es ser capaces de predecir y mejorar importantes factores de calidad de los artefactos de software y conocer las mejores prácticas de los proyectos del pasado (tanto si han tenido éxito como si no). El aprendizaje de estos factores se lleva a cabo por medio de la minería masiva de depósitos de software como GitHub (con más de 30 millones de proyectos en este momento).

La analítica de software incluye el análisis del código del programa, pero nos interesa especialmente estudiar todos los aspectos sociales y colaborativos que giran a su alrededor (quién es la comunidad que construye el software, cómo se organizan, cuáles son las mejores prácticas que siguen, etc.).