Software Verification and Testing

Course guarantor:

Lecturer:

Tutor:

Supervisor:

Department of Mathematics

Synopsis:

This course will introduce the theoretical foundations and mathematical concepts necessary for rigorous software testing, including the definitions of fundamental system characteristics, such as reliability, robustness and

correctness of the software system. We will emphasize the techniques and abstract tools necessary for validation of the correctness and reliability characteristics of the software. In the first part of the course, we will

introduce the existing techniques and paradigms for system testing (black/white box, formal methods, structural analysis), including the methods for test number reduction and automation. The second part of the course will concentrate on formal methods for system verification. We will introduce the formal frameworks necessary for the dynamic description of

system properties (Z-notation, temporal logic) and the applicable verification methods (model checking, theorem proving) working on these representations.

Requirements:

The online information can be found at: https://cw.fel.cvut.cz/wiki/courses/01tvs/start

Syllabus of lectures:

1. Introduction to software testing and validation

2. Software test cases optimization

3. Software defects, their characterization and

categorization. Correctness and usability criteria.

4. Structural testing

5. Testing of state machines

6. Model checking using Alloy

7. Model checking I. System UPPAAL

8. Model checking II. Temporal logic

9. Verification using UPPAAL

10. Z-notation

11. Verification system PVS

12. Object oriented testing

13. Software reliability

14. Statistical testing.

Syllabus of tutorials:

1. Organization, structure presentation

2. Presentation of testing and validation systems

3. Presentation of testing and validation systems

4. Presentation of testing and validation systems

5. Project definition and assignments - Project 1

6. Project work - Project 1

7. Project work - Project 1

8. Project work - Project 1

9. Project work - Project 1

10. Project definition and assignments - Project 2

11. Project work - Project 2

12. Project work - Project 2

13. Project work - Project 2

14. Grading

Study Objective:

Necessary mathematical, both theoretical and practical foundations of large scale software system testing are provided in this course, covering also its model specification and verification.

Study materials:

Paul Ammann and Jeff Offutt, Introduction to Software Testing, Cambridge University Press, Cambridge, UK, ISBN 0-52188-038-1, 2008.

Systems and Software Verification: Model-Checking Techniques and Tools by B. Berard, M. Bidoit, A. Finkel, and F. Laroussinie, Springer; 2001

Note:

Further information:

https://cw.fel.cvut.cz/wiki/courses/01tvs/start

No time-table has been prepared for this course

The course is a part of the following study plans: