Software Verification and Testing

Lecturer:

Radek Mařík (gar.)

Tutor:

Radek Mařík (gar.), Ivan Havel

Supervisor:

Department of Cybernetics

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 descripton of

system properties (Z-notation, temporal logic) and the applicable

verification methods (model checking, theorem proving) working on these

representations.

Requirements:

Syllabus of lectures:

1. Introduction to testing and validation

2. System requirements and specifications

3. Software defects, their characterization and

categorization. Correctness and usability criteria.

4. Black, grey and white box testing.

5. White box teting optmization. Structural analysis.

6. Static and dynamic analysis, data flow analysis.

7. Integration and load testing.

8. Formal program specifications, Z-notation, temporal logic.

9. Verification by automated theorem proving methods.

10. Verification automation by model checking.

11. Axiomatic and functional verification.

12. Verification of open and distributed systems.

13. Testing and verification tools.

14. Future of software tsting and verification.

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:

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:

Time-table for winter semester 2011/2012:

	06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Mon
Tue
Fri
Thu	roomKN:E-301 Mařík R. 12:45–14:15 (lecture parallel1) Karlovo nám. Šrámkova posluchárna K9roomKN:E-132 Mařík R. Havel I. 14:30–16:00 (lecture parallel1 parallel nr.101) Karlovo nám. Laboratoř PCroomKN:E-220 Mařík R. Havel I. 16:15–17:45 (lecture parallel1 parallel nr.102) Karlovo nám. Laboratoř BIOroomKN:E-220 18:00–19:30 (lecture parallel1 parallel nr.103) Karlovo nám. Laboratoř BIO
Fri

Time-table for summer semester 2011/2012:

Time-table is not available yet

The course is a part of the following study plans:

• Otevřená informatika - Softwarové inženýrství (compulsory course of the specialization)