Bajo el título Especificación de los Sistemas Software se presentan diversas metodologías y técnicas formales para especificar requisitos en distintas etapas del proceso de desarrollo de sistemas software.
Cada vez son más los desarrollos de software que requieren comprobación y verificación formal en alguna parte del producto. Sobre todo en aquellos proyectos que implican la gestión de sistemas críticos: transacciones, aviación y vuelos espaciales, plantas nucleares, etc.
Las diferentes metodologías de verificación se basan en diversas ampliaciones de la lógica clásica. El hacer uso de ellas requiere saber como expresar los requisitos a verificar en las gramáticas de estas lógicas.
Empezaremos con un repaso de las lógicas clásicas de primer orden: lógica proposicional y la lógica de predicados. Las futuras ampliaciones de estas lógicas las veremos dentro de su marco de utilización a lo largo de curso. Así, por ejemplo, estudiaremos la lógica temporal dentro de la verificación de sistemas concurrentes. En otros escenarios, en cambio, lo importante es verificar que el propio código funciona correctamente, para ello existen metodolologías y tecnologías llamadas verificadores de programas que utilizan una lógica proposicional modificada. En concreto, veremos en el curso la lógica de Hoare.
Contextualización:
La asignatura Especificación de los Sistemas Software se encuentra integrada en el Bloque de Ingeniería del Software dentro de la materia Ingeniería del Desarrollo del Software.
Tiene carácter anual y es de tipo optativo. El número de créditos ECTS que se consigue es 9, igual al resto de asignaturas del máster.
Sus contenidos están diseñados para capacitar la comprensión, alcance y limitación de la verificación formal de requisitos. Obteniendo así una visión general de las distintas soluciones que pudieran aparecer en los distintos ámbitos del Desarrollo del Software.
Estos métodos y soluciones específicos de la verificación dependen, principalmente, de la propia arquitectura del software, que los condicionará en gran medida. Es por ello que podemos afirmar que los contenidos de esta asignatura son completamente transversales a los del resto de asignaturas que forman la materia Ingeniería del Desarrollo de Software.
Esto significa, que sus contenidos no dependen de asignatura previas ni tiene continuación con otra asignatura. Se puede cursar y estudiar de forma independiente, ya su vez, resultará un buen complemento al resto de las asignaturas de su materia.
La introducción de métodos genéricos de especificación y verificación formal dentro del desarrollo software es relativamente nuevo. De hecho estos métodos provienen de otros campos de la ingeniería como Diseño Hardware, Ingeniería Industrial y también del propio desarrollo software pero en dominios de aplicación muy limitada. Es por ello que esta asignatura también se complementa perfectamente con otras materias del Máster como por ejemplo:
