Testování a verifikace software

Přednášející:

Radek Mařík (gar.)

Cvičící:

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

Předmět zajišťuje:

katedra kybernetiky

Anotace:

Předmět představí matematické a teoretické základy nutné pro zvládnutí

problematiky testování software, včetně definic základních pojmů

(spolehlivost, korektnost SW systému atd.) Důraz bude kladen na

nástroje a techniky použitelné pro vyhodnocení korektnosti a kvality

SW systémů. První část předmětu se zabývá existujícími metodami pro

testování (metody černé a bílé skříňky, formální metody, funkční a

strukturální analýza), včetně metod pro redukci počtu testů a jejich

automatizaci.Druhá část předmětu se soustředí na metody pro formální

verifikaci SW systémů. Budou probrány formalismy pro popis dynamických

vlastností SW systémů (Z-notace, temporální logiky) a mechanismy pro

jejich automatickou verifikaci (model checking, theorem proving).

Požadavky:

Aktuální informace najdete na:

http://labe.felk.cvut.cz/~marikr/teaching/A4M33TSV_10/A4M33TSV.htm

Osnova přednášek:

1. Úvod do testování a verifikace SW

2. Požadavky a specifikace na SW systém

3. Pojem chyby software, kategorizace chyb. Kritéria korektnosti a

použitelnosti.

4. Testování metodami černé, šedé a bílé skříňky

5. Efektivizace metod testování bílé skříňky. Strukturální

analýza. Invarianty a jejich omezení.

6. Statická a dynamická analýza. Analýza datových toků.

7. Integrační a zátěžové testy.

8. Formální specifikace programu: z-notace, temporální logiky

9. Verifikace metodami automatického dokazování

10. Automatická verifikace metodou model checking

11. Axiomatická a funkcionální verifikace

12. Verifikace distribuovaných a otevřených systémů

13. Nástroje pro testování a verifikaci SW

14. Otevřená témata v testování a verifikaci SW. Výhled do budoucna.

Osnova cvičení:

1. Organizace cvičení, podmínky zápočtu

2. Presentace systémů pro testování a verifikaci software

3. Presentace systémů pro testování a verifikaci software

4. Presentace systémů pro testování a verifikaci software

5. Zadání semestrální práce 1

6. Vypracování semestrální práce 1

7. Vypracování semestrální práce 1

8. Vypracování semestrální práce 1

9. Vypracování semestrální práce 1

10. Zadání semestrální práce 2

11. Vypracování semesterální práce 2

12. Vypracování semesterální práce 2

13. Vypracování semesterální práce 2

14. Udělení zápočtů

Cíle studia:

Studijní materiály:

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

Poznámka:

Rozsah výuky v kombinované formě studia: 14p+6c

Rozvrh na zimní semestr 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
Po
Út
St
Čt	místnost KN:E-301 Mařík R. 12:45–14:15 (přednášková par. 1) Karlovo nám. Šrámkova posluchárna K9místnost KN:E-132 Mařík R. Havel I. 14:30–16:00 (přednášková par. 1 paralelka 101) Karlovo nám. Laboratoř PCmístnost KN:E-220 Mařík R. Havel I. 16:15–17:45 (přednášková par. 1 paralelka 102) Karlovo nám. Laboratoř BIOmístnost KN:E-220 18:00–19:30 (přednášková par. 1 paralelka 103) Karlovo nám. Laboratoř BIO
Pá

Rozvrh na letní semestr 2011/2012:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Otevřená informatika - Softwarové inženýrství (povinný předmět oboru)