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).
Výsledek studentské ankety varianty předmětu na FEL je zde: A4M33TVS
Předmět představuje matematické, teoretické, a praktické základy nutné pro zvládnutí problematiky testování rozsáhlých softwarových systémů, jejich specifikace a verifikace modelů.
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 | 04.10.2017 | RM | Úvod do testování a verifikace SW. | Přehled P01.Úvod p00.tvsotazky.pdf |
2 | 11.10.2017 | RM | Optimalizace testovacích sad. | P02.Optimalizace.pdf |
3 | 18.10.2017 | RM | Strukturované testování. | P03.StrukturovaneTestovani.pdf |
4 | 25.10.2017 | RM | Testování stavových automatů. | P04.KonecneAutomaty.pdf |
5 | 01.11.2017 | RM | Specifikační jazyky - Alloy | P05.Alloy.pdf |
6 | 08.11.2017 | RM | Verifikace metodou model checking I Úvod do systému UPPAAL | P06.ModelChecking1.pdf |
7 | 15.11.2017 | nekoná se | ||
8 | 22.11.2017 | RM | Verifikace metodou model checking II Temporální logiky Verifikace metodou model checking III | P08.TemporalniLogika.pdf P09.ModelChecking3.pdf |
9 | 29.11.2017 | nekoná se | ||
10 | 06.12.2017 | RM | Formální metody - Z notace. Formální metody - PVS. | P10.FormalniMetodyZ.pdf P10.FormalniMetodyPVS.pdf |
11 | 13.12.2017 | RM | Softwarové chyby, kategorizace chyb. Tradiční metody testování. | P11.SoftwaroveChyby.pdf |
12 | 20.12.2017 | RM | Testování objektově-orientovaného softwaru. | P12.OOTestovani.pdf |
13 | 03.01.2018 | RM | Hodnocení spolehlivosti softwaru. Statistické testování | P13.StatistickeTestovani.pdf P13.Spolehlivost.pdf |
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 | 04.10.2017 | RM | Organizace cvičení. Kontrola přístupu do laboratoře a k počítačům. Instalace prostředí. Instalace UPPAAL. Kontrola přístupu k Upload systému. | ||
2 | 11.10.2017 | RM | 6 | Optimalizace pomocí ortogonálních polí a latinských čtverců. | Optimalizace.pdf |
3 | 28.10.2017 | RM | 4 | Vytváření testů pro řídicí tok. | ControlFlow.pdf |
4 | 25.10.2017 | RM | 4 | Vytváření testů pro datový tok. | DataFlow.pdf |
5 | 01.11.2017 | RM | 8 | Testování stavového automatu – I. | TestovaniFSM.pdf Automaty |
6 | 08.11.2017 | RM | 8 | Alloy | AlloyZadani.pdf Alloy Cheat Sheet1) A01.pdf A02.pdf A03.pdf A04.pdf A05.pdf A06.pdf A07.pdf A08.pdf A09.pdf A10.pdf |
7 | 15.11.2017 | domácí práce bez konzultace | |||
8 | 22.11.2017 | RM | 2 | Model checking (Uppaal) – modelová úloha (příprava: nainstalujte si Uppaal) | VariantyNIM.pdf uppaal_cviceni.ppsx uppaal_cviceni.pdf hra_nim.q hra_nim.xml Biphase_Mark_Protocol.xml Biphase_Mark_Protocol.q u01.dimacs95.pdf u02.v3i9-0466.pdf u03.10.1007_s00165-006-0008-1.pdf u04.lpw-tacas98.pdf u05.bo-case.pdf u06.cs1.pdf u07.fokkink.pdf u08.w115.pdf u10.fates03.pdf u11.10.1007_978-3-642-16558-0_47.pdf u12.msu-cse-13-7.ps uppaalzadani.pdf |
9 | 29.11.2017 | domácí práce bez konzultace | |||
10 | 06.12.2017 | RM | 8 | Model checking – semestrální úloha Alloy – předávání úloh | |
11 | 13.12.2017 | RM | Model checking – semestrální úloha | ||
12 | 20.12.2017 | RM | Model checking – semestrální úloha, předávání úloh | ||
13 | 03.01.2018 | RM | Model checking – předávání úloh | ||
14 | 10.01.2018 | RM | Předávání úloh opozdilců |
ČVUT hodnotící tabulka:
Body | >=90 | <80, 90) | <70, 80) | <60, 70) | <50, 60) | (0, 50) |
---|---|---|---|---|---|---|
Známka | A | B | C | D | E | F |