Na convocatoria de primeira oportunidade, en caso de non acadar o mínimo na proba obxectiva, a nota final será a obtida na proba obxectiva.

Na convocatoria de segunda oportunidade, a proba obxectiva terá un peso do 80% nos casos nos que a avaliación
continua e de prácticas de laboratorio sume un total inferior
a 1 punto, a fin de garantir o dereito das/os estudantes a superar a materia.

De acordo coa normativa da UDC en relación ao estudantado matriculado a tempo parcial, o réxime de asistencia a clase non afectará negativamente ao proceso de avaliación, admitíndose nesta materia a dispensa académica para a asistencia solicitada polas canles institucionais habilitadas ao efecto. Porén, esta flexibilidade asistencial non eximirá da entrega de traballos tutelados e prácticas nos mesmos prazos fixados para o estudantado a tempo completo.

Así mesmo, segundo
se recolle nas distintas normativas de aplicación para a docencia
universitaria, a incorporación da perspectiva de xénero nesta materia aplicarase empregando unha linguaxe non sexista e propiciando a intervención durante as sesións maxistrais de alumnas e
alumnos de xeito equilibrado. Traballarase
para identificar e modificar prexuízos e actitudes sexistas, e
influirase na contorna para modificalos e fomentar valores de respecto e
igualdade. Finalmente, caso de se detectaren situacións de discriminación por razón de xénero, proporanse accións e medidas para corrixilas.

Resultados de aprendizaxe	Competencias / Resultados do título
Capacidade de identificar e analizar problemas e deseñar, desenvolver, implementar, verificar e documentar solucións software sobre a base dun coñecemento axeitado das teorías, modelos e técnicas actuais.	A28	B1 B3	C2 C3 C6 C7 C8

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 requirimentos I1.3. Automatización 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, razoamento 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

Metodoloxías / probas	Competencias / Resultados	Horas lectivas (presenciais e virtuais)	Horas traballo autónomo	Horas totais
Sesión maxistral	B3 C2 C7 C8	21	26.25	47.25
Prácticas de laboratorio	A28 B1 B3 C2 C3 C6	21	42	63
Proba obxectiva	B1 B3 C6	3	31.5	34.5

Atención personalizada		5.25	0	5.25

*Os datos que aparecen na táboa de planificación son de carácter orientativo, considerando a heteroxeneidade do alumnado

Metodoloxías	Descrición
Sesión maxistral	Clases de teoría onde se imparten os contidos do temario.
Prácticas de laboratorio	Elaboración de traballos prácticos no laboratorio.
Proba obxectiva	Exame escrito.

Metodoloxías	Competencias / Resultados	Descrición	Cualificación
Proba obxectiva	B1 B3 C6	Exame escrito que computa 4 puntos da nota final. Require un mínimo de 2 puntos para superar a materia.	40
Prácticas de laboratorio	A28 B1 B3 C2 C3 C6	Entrega e defensa de traballos prácticos de laboratorio. Computa 6 puntos da nota final, 2 puntos por bloque de contidos da materia. A súa realización non é obrigatoria para superar a materia.	60

Observacións avaliación
Na convocatoria de primeira oportunidade, en caso de non acadar o mínimo na proba obxectiva, a nota final será a obtida na proba obxectiva. Na convocatoria de segunda oportunidade, a proba obxectiva terá un peso do 80% nos casos nos que a avaliación continua e de prácticas de laboratorio sume un total inferior a 1 punto, a fin de garantir o dereito das/os estudantes a superar a materia. De acordo coa normativa da UDC en relación ao estudantado matriculado a tempo parcial, o réxime de asistencia a clase non afectará negativamente ao proceso de avaliación, admitíndose nesta materia a dispensa académica para a asistencia solicitada polas canles institucionais habilitadas ao efecto. Porén, esta flexibilidade asistencial non eximirá da entrega de traballos tutelados e prácticas nos mesmos prazos fixados para o estudantado a tempo completo. Así mesmo, segundo se recolle nas distintas normativas de aplicación para a docencia universitaria, a incorporación da perspectiva de xénero nesta materia aplicarase empregando unha linguaxe non sexista e propiciando a intervención durante as sesións maxistrais de alumnas e alumnos de xeito equilibrado. Traballarase para identificar e modificar prexuízos e actitudes sexistas, e influirase na contorna para modificalos e fomentar valores de respecto e igualdade. Finalmente, caso de se detectaren situacións de discriminación por razón de xénero, proporanse accións e medidas para corrixilas.

Bibliografía básica	Crispin Lisa, Gregory Janet (2008). Agile Testing: A Practical Guide for Testers and Agile Teams. Addison-Wesley Maurício Aniche (2022). Effective software testing. Manning Gayathri Mohan (2022). Full Stack Testing. O'Reilly Media, Inc. Mordechai Ben-Ari (2012). Mathematical Logic for Computer Science. Springer Mordechai Ben-Ari (2001). Mathematical Logic for Computer Science. Springer Charity Majors, Liz Fong-Jones, George Miranda (2022). Observability Engineering. O'Reilly Media, Inc. Fred Hébert (2019). Property-based testing with PropEr, Erlang, and Elixir : find bugs before your users do. The Pragmatic Bookshelf Brian Okken (2022). Python testing with pytest. The Pragmetic Programmers Kent Beck (2002). Test Driven Development (By Example). Addison-Wesley Gerard J. Holzmann (2003). The SPIN model checker: primer and reference manual. Addison-Wesley Zohar Manna and Amir Pnueli (1995). The Temporal Logic of Reactive and Concurrent Systems. Safety. Springer Zohar Manna and Amir Pnueli (1991). The Temporal Logic of Reactive and Concurrent Systems. Specification. Springer

Bibliografía complementaria

Observacións