Guía DocenteCurso Facultade de Informática |
Grao en Enxeñaría Informática |
![]() |
![]() |
![]() |
|
|
|
Datos Identificativos | 2024/25 | |||||||||||||
Asignatura | Validación e Verificación do Software | Código | 614G01225 | |||||||||||
Titulación |
|
|||||||||||||
Descriptores | Ciclo | Período | Curso | Tipo | Créditos | |||||||||
Grao | 2º cuadrimestre |
Cuarto | Obrigatoria | 6 | ||||||||||
|
Temas | Subtemas |
Bloque I: Validación de software |
I.1 Especificación, deseño e execución de probas I1.1. Niveis e tipos de probas I1.2. Propiedades e trazabilidade de requerimentos I.2 Xestión de probas: planificación, avaliación, métricas e revisións |
Bloque II: Métodos formais e razonamento automático |
II.1 Introdución: Dedución natural e cálculo de secuentes II.2 Proba automática utilizando PVS II.3 Que é e para que se utiliza un probador de teoremas? II.4 Linguaxe de especificación de PVS: Tipos, expresións, teorías, subtipado II.5 Probador PVS: tácticas, recursión, razonamento ecuacional |
Bloque III: Comprobación por modelos (model checking) | III.1 Introdución ás lóxicas modais temporais III.2 Especificación de propiedades: deadlocks, safety, liveness, fairness III.3 Funcionamento dun comprobador por modelos III.4 Introdución ao manexo dunha ferramenta de model checking |
|