|
Teaching GuideTerm Faculty of Computer Science |
| Grao en Enxeñaría Informática |
 Subjects |
| Software Verification and Validation |
| Contents |
|
|
|
| Identifying Data | 2020/21 | |||||||||||||
| Subject | Software Verification and Validation | Code | 614G01053 | |||||||||||
| Study programme |
|
|||||||||||||
| Descriptors | Cycle | Period | Year | Type | Credits | |||||||||
| Graduate | 1st four-month period |
Fourth | Optional | 6 | ||||||||||
|
||||||||||||||
| 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 |
|
