Table of Contents

A4M33TVS: Testování a verifikace software

Přednášky

Informace o přednáškách a cvičeních předmětu z minulých let lze nalézt na stránce: A4M33TVS

Týden Datum Přednášející Obsah přednášky Výukové materiály
1 06.10.2016 RM Úvod do testování a verifikace SW. 01.uvod.pdftvsotazky.pdf
2 13.10.2016 RM Optimalizace testovacích sad. 02.optimalizace.pdf
3 20.10.2016 RM Strukturované testování. 04.strukturovanetestovani.pdf
4 27.10.2016 RM Testování stavových automatů. 06.konecneautomaty.pdf
chapter-3.ppt
5 03.11.2016 RM Specifikační jazyky - Alloy 05.alloy.pdf
6 10.11.2016 RM Softwarové chyby, kategorizace chyb. 
Tradiční metody testování.
03.softwarovechyby.pdf
7 17.11.2016 (státní svátek)
8 24.11.2016 Vyskočil Verifikace metodou model checking I 07.modelchecking1.pdf
9 01.12.2016 Vyskočil Verifikace metodou model checking II 
Temporální logiky
08.temporalnilogika.pdf
10 08.12.2016 RM? Verifikace metodou model checking III 09.modelchecking3.pdf
11 15.12.2016 RM JPF – generování testovacích případů 11.javapathfinder.pdf
12 22.12.2016 RM Formální metody - Z notace. 
Formální metody - PVS.
10.formalnimetodyz.pdf
11.formalnimetodypvs.pdf
13 05.01.2017 RM Testování objektově-orientovaného softwaru. 12.ootestovani.pdf
14 12.01.2017 RM Hodnocení spolehlivosti softwaru. 
Statistické testování
13.spolehlivost.pdf
13.statisticketestovani.pdf

Cvičení

Odevzdávaným výstupem každé úlohy je zpráva (PDF, HTML, plain text), kde je vedle samozřejmých částí, jako je zadání úlohy, závěr nebo jména autorů, uvedeno jak jste úlohu řešili, k jakým výsledkům jste došli, na jaké potíže jste narazili a jak jste se s nimi vypořádali. Zpráva by měla být co nejkratší, ale nesmí v ní nic podstatného chybět. Součástí bodového hodnocení úlohy je kvalita zpracování zprávy.

Na cvičení budete potřebovat Uppaal, Alloy a váš oblíbený skriptovací jazyk pro generování zpráv. Také by se vám mohl hodit Graphviz.

Deadline pro odevzdání úlohy je obvykle následující cvičení. Výjimkami jsou Alloy a semestrální úloha.

Týden Datum Cvičící Body za úlohu Obsah Výukové materiály
1 06.10.2016 RM,RM Organizace cvičení. Rozdělení do skupin po max. 3 studentech. Kontrola přístupu do laboratoře a k počítačům. Instalace prostředí. Instalace UPPAAL. Kontrola přístupu k Upload systému.
2 13.10.2016 RM,RM 6 Optimalizace pomocí ortogonálních polí a latinských čtverců. UlohyOptimalizace.pdf
3 20.10.2016 RM,RM 4 Vytváření testů pro řídicí tok. sttCfgUlohy.pdf
4 27.10.2016 RM,RM 4 Vytváření testů pro datový tok. sttDfgUlohy.pdf
5 03.11.2016 RM,RM 8 Alloy alloyZadani.pdf
Alloy Cheat Sheet1)
6 10.11.2016 JK,JK 8
Testování stavového automatu – I.
Výběr téma semestrální práce
state-machine
severzde_2012dipl.pdf
7 17.11.2016 (státní svátek)
8 24.11.2016 JK,JK Testování stavového automatu – II.
9 01.12.2016 JK,JK

10
Model checking (Uppaal) – modelová úloha
(příprava: nainstalujte si Uppaal)
Zadání semestrální práce
VariantyNIM.pdf
uppaal_cviceni.ppsx
uppaal_cviceni.pdf
hra_nim.q
hra_nim.xml
Biphase_Mark_Protocol.xml
Biphase_Mark_Protocol.q
10 08.12.2016 JK,JK Model checking – semestrální úloha
11 15.12.2016 RM,RM Alloy – předávání úloh 
Model checking – semestrální úloha
12 22.12.2016 JK,JK Model checking – semestrální úloha, předávání úloh
13 05.01.2017 JK,JK Model checking – předávání úloh
14 12.01.2017 RM+JK,RM+JK Zápočty, předávání úloh opozdilců

Podmínky zápočtu

Výsledná známka u zkoušky

1)
Patche vítány. Pokud vám v cheat sheetu něco chybí, není jasné nebo je špatně, napište mi, nebo rovnou pošlete merge request v odkazovaném repositáři.