| Study programme competencies |
|
Code
|
Study programme competences
|
| A28 |
Capacidade de identificar e analizar problemas, e deseñar, desenvolver, implementar, verificar e documentar solucións sóftware sobre a base dun coñecemento adecuado das teorías, modelos e técnicas actuais. |
| B1 |
Capacidade de resolución de problemas |
| B3 |
Capacidade de análise e síntese |
| C2 |
Dominar a expresión e a comprensión de forma oral e escrita dun idioma estranxeiro. |
| C3 |
Utilizar as ferramentas básicas das tecnoloxías da información e as comunicacións (TIC) necesarias para o exercicio da súa profesión e para a aprendizaxe ao longo da súa vida. |
| C6 |
Valorar criticamente o coñecemento, a tecnoloxía e a información dispoñible para resolver os problemas cos que deben enfrontarse. |
| C7 |
Asumir como profesional e cidadán a importancia da aprendizaxe ao longo da vida. |
| C8 |
Valorar a importancia que ten a investigación, a innovación e o desenvolvemento tecnolóxico no avance socioeconómico e cultural da sociedade. |
| Learning aims |
| Learning outcomes |
Study programme competences |
| Ability to identify and analise problems, and to design, develop, implement, validate and document software solutions on the basis of an deep understanding and knowledge of modern theories, models and techniques.
|
A28
|
B1
B3
|
C2
C3
C6
C7
C8
|
| Contents |
| Topic |
Sub-topic |
Part I: Software Validation
|
I.1 Test secification, design and execution
I1.1. Levels and types of tests
I1.2. Properties and traceability of requirements
I1.3. Automation
I.2 Test management: planning, assessment, metrics and reviews |
Part II: Formal methods and automatic reasoning
|
II.1 Introduction: natural deduction and calculus of sequences
II.2 Automatic proofs using PVS
II.3 What is a theorem prover and what is it used for?
II.4 PVS specification language: types, expressions, theories, subtyping
II.5 PVS prover: tactics, recursion, ecuational reasoning |
| Part III: Model checking |
III.1 Introduction to modal temporal logic
III.2 Properties specification: deadlocks, safety, liveness, fairness
III.3 How a model checker works
III.4 Introduction to the use of a model checking tool |
| Planning |
| Methodologies / tests |
Competencies |
Ordinary class hours |
Student’s personal work hours |
Total hours |
| Guest lecture / keynote speech |
B3 C2 C7 C8 |
21 |
26.25 |
47.25 |
| Laboratory practice |
A28 B1 B3 C2 C3 C6 |
14 |
35 |
49 |
| Supervised projects |
A28 B1 B3 C2 C3 C6 |
7 |
7 |
14 |
| Objective test |
B1 B3 C6 |
3 |
31.5 |
34.5 |
| |
| Personalized attention |
|
5.25 |
0 |
5.25 |
| |
| (*)The information in the planning table is for guidance only and does not take into account the heterogeneity of the students. |
| Methodologies |
|
Methodologies |
Description |
| Guest lecture / keynote speech |
Master class where the theoretical contents of the study programme are presented. |
| Laboratory practice |
Hands-on work sessions in the lab. |
| Supervised projects |
Student assignments to be done during reduced-group classes. |
| Objective test |
Written test. |
| Personalized attention |
|
Methodologies
|
| Objective test |
| Supervised projects |
| Guest lecture / keynote speech |
| Laboratory practice |
|
| Description |
Questions/answers about the theoretical/practical aspects of the subjects, during the corresponding office hours of each teacher.
Part-time students should be able to follow this subject without issues, given that attendance is not mandatory nor awarded qualification. However, part-time students are responsible for keeping up-to-date with the materials posted on the Moodle platform, as well as the assigments to be handed in. When the assignments are to be handed in by means other than telematic, they will be set up between part-time students and teachers to the best both their schedules allow.
|
|
| Assessment |
|
Methodologies
|
Competencies |
Description
|
Qualification
|
| Objective test |
B1 B3 C6 |
Written test, up to a maximum of 4 points in the final score. A minimum of 2 points is required to pass. |
40 |
| Supervised projects |
A28 B1 B3 C2 C3 C6 |
Presentation and participation in student assignments, performed during reduced-group classes, up to a maximum of 2 points in the final score. These are not compulsory to pass. |
20 |
| Laboratory practice |
A28 B1 B3 C2 C3 C6 |
Hand in and presentation of hands-on student assignments, up to a maximum of 4 points in the final score. These are not compulsory to pass. |
40 |
| |
|
Assessment comments |
Those students who do not reach the minimum in the objective test, will be qualified with the qualification they obtain in that objective test. In the second opportunity, the objective test may include a specific evaluation of the laboratory practice. In compliance with the academic rules at UDC that apply to part-time students, physical presence in the classroom/laboratory will not be regarded as qualification element. That is to say, students may officially apply to be dismissed from attending lectures and laboratory practices. All in all, part-time students will still need to comply with deadlines established for supervised projects and laboratory projects. |
| Sources of information |
|
Basic
|
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
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
|
|
|
Complementary
|
|
|
| Recommendations |
| Subjects that it is recommended to have taken before |
| Software Design/614G01015 | | Concurrency and Parallelism/614G01018 | | Software Process/614G01019 | | Software Architecture/614G01221 | | Requirements Engineering/614G01222 | | Quality Assurance/614G01223 |
|
| Subjects that are recommended to be taken simultaneously |
| Knowledge Representation and Automatic Reasoning/614G01036 | | Theoretical Computer Science/614G01039 | | Development Methodologies/614G01051 |
|
| Subjects that continue the syllabus |
| Software Development Projects/614G01226 |
|
|