| Competencias del título |
|
Código
|
Competencias del título
|
| A28 |
Capacidad de identificar y analizar problemas, y diseñar, desarrollar, implementar, verificar y documentar soluciones software sobre la base de un conocimiento adecuado de las teorías, modelos y técnicas actuales. |
| B1 |
Capacidad de resolución de problemas |
| B3 |
Capacidad de análisis y síntesis |
| C2 |
Dominar la expresión y la comprensión de forma oral y escrita de un idioma extranjero. |
| C3 |
Utilizar las herramientas básicas de las tecnologías de la información y las comunicaciones (TIC) necesarias para el ejercicio de su profesión y para el aprendizaje a lo largo de su vida. |
| C6 |
Valorar críticamente el conocimiento, la tecnología y la información disponible para resolver los problemas con los que deben enfrentarse. |
| C7 |
Asumir como profesional y ciudadano la importancia del aprendizaje a lo largo de la vida. |
| C8 |
Valorar la importancia que tiene la investigación, la innovación y el desarrollo tecnológico en el avance socioeconómico y cultural de la sociedad. |
| Resultados de aprendizaje |
| Resultados de aprendizaje |
Competencias del título |
| Capacidad de identificar y analizar problemas y deseñar, desarrollar, implementar, verificar y documentar soluciones software sobre la base de un conocimiento apropiado de las teorías, modelos y técnicas actuales. |
A28
|
B1
B3
|
C2
C3
C6
C7
C8
|
| Contenidos |
| Tema |
Subtema |
Bloque I: Validación de software
|
I.1 Especificación, diseño y ejecución de pruebas
I1.1. Niveles y tipos de pruebas
I1.2. Propiedades y trazabilidad de requisitos
I1.3. Automatización
I.2 Gestión de pruebas: planificación, evaluación, métricas y revisiones |
Bloque II: Métodos formales y razonamiento automático
|
II.1 Introducción: Deducción natural y cálculo de secuentes
II.2 Prueba automática utilizando PVS
II.3 ¿Qué és y para que se utiliza un probador de teoremas?
II.4 Lenguaje de especificación de PVS: Tipos, expresiones, teorías, subtipado
II.5 Probador PVS: tácticas, recursión, razonamiento ecuacional |
| Bloque III: Comprobación por modelos (model checking) |
III.1 Introducción a las lógicas modales temporales
III.2 Especificación de propiedades: deadlocks, safety, liveness, fairness
III.3 Funcionamiento de un comprobador por modelos
III.4 Introducción al manejo de una herramienta de model checking |
| Planificación |
| Metodologías / pruebas |
Competéncias |
Horas presenciales |
Horas no presenciales / trabajo autónomo |
Horas totales |
| Sesión magistral |
B3 C2 C7 C8 |
21 |
26.25 |
47.25 |
| Prácticas de laboratorio |
A28 B1 B3 C2 C3 C6 |
14 |
35 |
49 |
| Trabajos tutelados |
A28 B1 B3 C2 C3 C6 |
7 |
7 |
14 |
| Prueba objetiva |
B1 B3 C6 |
3 |
31.5 |
34.5 |
| |
| Atención personalizada |
|
5.25 |
0 |
5.25 |
| |
| (*)Los datos que aparecen en la tabla de planificación són de carácter orientativo, considerando la heterogeneidad de los alumnos |
| Metodologías |
|
Metodologías |
Descripción |
| Sesión magistral |
Clases de teoría donde se imparten los contenidos del temario. |
| Prácticas de laboratorio |
Elaboración de trabajos prácticos en el laboratorio. |
| Trabajos tutelados |
Resolución de trabajos tutelados planteados y resueltos en horario de tutorías de grupos reducidos. |
| Prueba objetiva |
Examen escrito. |
| Atención personalizada |
|
Metodologías
|
| Prueba objetiva |
| Trabajos tutelados |
| Sesión magistral |
| Prácticas de laboratorio |
|
| Descripción |
Resolución de dudas de teoría y/o prácticas, trabajos tutelados, etc. en horario de tutorías de cada profesor/a.
El seguimiento de la asignatura no debe presentar problemas al estudiantado con matrícula a tiempo parcial, ya que no se exige ni se puntúa la asistencia. Sin embargo, este alumnado es responsable de estar al corriente de los materiales colgados en el Moodle, así como de las tareas que por ese medio se propongan para entrega. Estas entregas, de no ser telemáticas, serán acordadas con el estudiantado a tiempo parcial de modo que se compatibilice en la medida de lo posible con su disponibilidad y la del profesorado. |
|
| Evaluación |
|
Metodologías
|
Competéncias |
Descripción
|
Calificación
|
| Prueba objetiva |
B1 B3 C6 |
Examen escrito que computa un máximo de 4 puntos sobre la nota final. Se requiere un mínimo de 2 puntos para superar la asignatura. |
40 |
| Trabajos tutelados |
A28 B1 B3 C2 C3 C6 |
Resolución y participación en trabajos tutelados en horario de tutorías de grupos reducidos. Computa un máximo de 2 puntos de la nota final. Su realización no es obligatoria para superar la asignatura. |
20 |
| Prácticas de laboratorio |
A28 B1 B3 C2 C3 C6 |
Entrega e defensa de trabajos prácticos de laboratorio. Computa hasta un máximo de 4 puntos de la nota final. Su realización no es obligatoria para superar la asignatura. |
40 |
| |
|
Observaciones evaluación |
En caso de no alcanzar el mínimo en la prueba objetiva, la nota final será a obtenida en la prueba objetiva. En la convocatoria de segunda oportunidad, la prueba objetiva irá
acompañada de una actividad de evaluación de las prácticas de laboratorio. De acuerdo con la normativa de la UDC en relación al estudiantado matriculado a tempo parcial, el régimen de asistencia a clase no afectará negativamente al proceso de evaluación, admitiéndose en esta asignatura la dispensa académica para la asistencia, solicitada por las vías institucionales habilitadas al efecto. Sin embargo, esta flexibilidad asistencial no eximirá de la entrega de trabajos tutelados y prácticas de laboratorio en los mismos plazos fijados para el estudiantado a tiempo completo. |
| Fuentes de información |
|
Básica
|
Peter Farrell-Vinay (2008). Manage software testing. Auerbach
Mordechai Ben-Ari (2012). Mathematical Logic for Computer Science. Springer
Mordechai Ben-Ari (2001). Mathematical Logic for Computer Science. Springer
Hébert, Fred (2019). Property-based testing with PropEr, Erlang, and Elixir : find bugs before your users do. The Pragmatic Bookshelf
Ron Patton (2001). Software testing. Sams
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
|
|
|
Complementária
|
|
|
| Recomendaciones |
| Asignaturas que se recomienda haber cursado previamente |
| Diseño Software/614G01015 | | Concurrencia y Paralelismo/614G01018 | | Proceso Software/614G01019 | | Arquitectura del Software/614G01221 | | Ingeniería de Requisitos/614G01222 | | Aseguramiento de la Calidad/614G01223 |
|
| Asignaturas que se recomienda cursar simultáneamente |
| Representación del Conocimiento y Razonamiento Automático/614G01036 | | Teoría de la computación/614G01039 | | Metodologías de Desarrollo/614G01051 |
|
| Asignaturas que continúan el temario |
| Proyectos de Desarrollo Software/614G01226 |
|
|