Competencies / Study results |
Code
|
Study programme competences / results
|
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 / results |
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 specification, 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 / Results |
Teaching hours (in-person & virtual) |
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 |
21 |
42 |
63 |
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. |
Objective test |
Written test. |
Personalized attention |
Methodologies
|
Objective test |
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 assignments to be handed in. When the assignments are to be handed in by means other than telematics, they will be set up between part-time students and teachers to the best both their schedules allow.
|
|
Assessment |
Methodologies
|
Competencies / Results |
Description
|
Qualification
|
Objective test |
B1 B3 C6 |
Written test, up to 4 points in the final score. A minimum of 2 points is required to pass. |
40 |
Laboratory practice |
A28 B1 B3 C2 C3 C6 |
Hand in and presentation of hands-on student assignments, up to 6 points in the final score (2 points per content topic). These are not compulsory to pass. |
60 |
|
Assessment comments |
In the first opportunity, students that do not reach the minimum in the objective test, will receive the mark they obtain in that objective test. In the second opportunity, the objective test will have a weight of 80% for those students which continuous and lab evaluation sums up less than 1 point, in order to guarantee their right to pass the subject. 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 a 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. Likewise, as stated in the different regulations applicable to university teaching, the incorporation of the gender perspective in this subject will be enforced by using non-sexist language and encouraging the intervention, during the master sessions, of women and men in a balanced way. We will work to identify and modify prejudices and sexist attitudes, and we will influence the environment to modify them and promote values of respect and equality. Finally, if situations of gender-based discrimination are detected, actions and measures will be proposed to correct them.
|
Sources of information |
Basic
|
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 |
|
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 |
|
|