Accesos directos a las distintas zonas del curso
Ir a los contenidos
Ir a menú navegación principal
Ir a menú pie de página
Subject's code : 31105024
En este bloque repasaremos los conceptos básicos de la Ingeniería del software vistos el cursos anteriores.
El objetivo es intentar esclarecer o definir en que consiste la especificación.
Los principales sistemas formales de verificación tienen como lenguaje de especificación alguna extensión de la lógica clásica. En esta unidad repasaremos la lógica clásica: la proposicional y de predicados. La funcionalidad de muchos sistemas o modelos vienen muy bien descritos mediante las expresiones lógicas.
Diferenciar bien los conceptos de demostración o inferencia frente a la deducción lógica o semántica es clave para entender el concepto de modelo en lógica.
En este bloque estudiaremos los sistemas de verificación agrupados bajo el nombre de model checking. Esta técnica consiste en crear un modelo del sistema, codificar la propiedad a estudiar (requisito) en el lenguaje del entorno y ver si el modelo satisface dicha propiedad.
En general las técnicas de verificación mediante el examen de modelos utilizan un sistema formal basado en la lógica temporal.
En los sistemas secuenciales que manipulan grandes cantidades de información con datos complejos, el posible espacio de estados que describiría el sistema en cada momento concreto (dando valor a todas la variables) sería muy grande y por tanto intratable de forma práctica. Por eso no sería posible obtener un modelo global del sistema.
Verificar una propiedad en estos sistemas se consigue construyendo una prueba de la misma dentro del un sistema de cálculo de un sistema formal. Del éxito o no de conseguir dicha prueba diremos que el sistema satisface o no la propiedad.
Por último veremos como, a partir de la lógica temporales, aparecieron otro tipo de lógicas con una semántica distinta que nos permitirán modelizar otros aspectos de interés de un sistema.
