====== 01TVS: Testování a verifikace software ====== * [[http://geraldine.fjfi.cvut.cz/bk/index.php?type=P&file=NMS_MINF_1.doc&lang=cz|FJFI předmět]] * [[http://cw.felk.cvut.cz/upload/|Odevzdávání úloh]] * [[https://cw.felk.cvut.cz/forum|Diskusní fórum]] * [[http://www.krbalek.cz/TimeTable/TT_people/KMMarik.pdf|Rozvrh]] ===== 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). Výsledek studentské ankety varianty předmětu na FEL je zde: [[https://www.fel.cvut.cz/cz/anketa/aktualni/courses/A4M33TVS|A4M33TVS]] ===== Cíle kurzu ===== 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ů. ===== Organizace kurzu ===== * Povinně volitelný předmět. * Kurz je zakončen **zápočtem** a **zkouškou**. * Absolvování kurzu je ohodnoceno **6 kredity**. * Kredity odpovídají 2 hodinám přednášky, 2 hodinám laboratoří and přibližně **5 hodinám domácí přípravy** každý týden. ===== 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: [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/A4M33TVS.htm|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. | {{:courses:01tvs:lectures:p00.tvs.pdf|Přehled}} \\ {{:courses:01tvs:lectures:p01.uvod.pdf|P01.Úvod}} {{:courses:01tvs:lectures:P00.TVSOtazky.pdf|}}| | 2 | 11.10.2017 | RM | Optimalizace testovacích sad. | {{:courses:01tvs:lectures:p02.optimalizace.pdf|P02.Optimalizace.pdf}}| | 3 | 18.10.2017 | RM | Strukturované testování. | {{:courses:01tvs:lectures:p03.strukturovanetestovani.pdf|P03.StrukturovaneTestovani.pdf}} | | 4 | 25.10.2017 | RM | Testování stavových automatů. | {{:courses:01tvs:lectures:p04.konecneautomaty.pdf| P04.KonecneAutomaty.pdf}} | | 5 | 01.11.2017 | RM | Specifikační jazyky - Alloy | {{:courses:01tvs:lectures:p05.alloy.pdf|P05.Alloy.pdf}} | | 6 | 08.11.2017 | RM | Verifikace metodou model checking I \\ Úvod do systému UPPAAL | {{:courses:01tvs:lectures:p06.modelchecking1.pdf|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 | {{:courses:01tvs:lectures:p08.temporalnilogika.pdf|P08.TemporalniLogika.pdf}} \\ {{:courses:01tvs:lectures:p09.modelchecking3.pdf|P09.ModelChecking3.pdf}}| | 9 | 29.11.2017 | | nekoná se | | | 10 | 06.12.2017 | RM | Formální metody - Z notace. \\ Formální metody - PVS. | {{:courses:01tvs:lectures:p10.formalnimetodyz.pdf|P10.FormalniMetodyZ.pdf}} \\ {{:courses:01tvs:lectures:p10.formalnimetodypvs.pdf| P10.FormalniMetodyPVS.pdf}} | | 11 | 13.12.2017 | RM | Softwarové chyby, kategorizace chyb. \\ Tradiční metody testování. | {{:courses:01tvs:lectures:p11.softwarovechyby.pdf| P11.SoftwaroveChyby.pdf}} | | 12 | 20.12.2017 | RM | Testování objektově-orientovaného softwaru. |{{:courses:01tvs:lectures:p12.ootestovani.pdf| P12.OOTestovani.pdf}} | | 13 | 03.01.2018 | RM | Hodnocení spolehlivosti softwaru. \\ Statistické testování | {{:courses:01tvs:lectures:p13.statisticketestovani.pdf|P13.StatistickeTestovani.pdf}} \\ {{:courses:01tvs:lectures:p13.spolehlivost.pdf|P13.Spolehlivost.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 [[http://www.rouming.cz/roumingShow.php?file=Essential_advise.jpg|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 [[http://www.uppaal.org/|Uppaal]], [[http://alloy.mit.edu/alloy/|Alloy]] a váš oblíbený skriptovací jazyk pro generování zpráv. Také by se vám mohl hodit [[http://www.graphviz.org/|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ů. |{{:courses:01tvs:seminars:ulohyoptimalizace.pdf|Optimalizace.pdf}} | | 3 | 28.10.2017 | RM | 4 | Vytváření testů pro řídicí tok. | {{:courses:01tvs:seminars:sttcfgulohy.pdf|ControlFlow.pdf}} | | 4 | 25.10.2017 | RM | 4 | Vytváření testů pro datový tok. | {{:courses:01tvs:seminars:sttdfgulohy.pdf|DataFlow.pdf}} | | 5 | 01.11.2017 | RM | 8 | Testování stavového automatu – I. | {{:courses:01tvs:seminars:fsmulohy2.pdf|TestovaniFSM.pdf}}\\ {{:courses:01tvs:seminars:fsm2.zip|Automaty}} | | 6 | 08.11.2017 | RM | 8 | Alloy | {{:courses:01tvs:seminars:alloyzadani.pdf|AlloyZadani.pdf}} \\ [[https://git.frozen-doe.net/jk/alloy-cheat-sheet/blob/master/alloy-cheatsheet.pdf|Alloy Cheat Sheet]]((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.)) \\ {{:courses:01tvs:seminars:a01.10.1.1.749.5393.pdf|A01.pdf}} {{:courses:01tvs:a02.10.1007_978-3-642-04912-5_6.pdf|A02.pdf}} \\ {{:courses:01tvs:a03.10.1007_978-3-642-17773-6_4.pdf|A03.pdf}} {{:courses:01tvs:a04.10.1007_s00165-007-0058-z.pdf|A04.pdf}} \\ {{:courses:01tvs:a05.500_lines_or_less_the_same-origin_policy.pdf|A05.pdf}} {{:courses:01tvs:a06.1407.5074.pdf|A06.pdf}} \\ {{:courses:01tvs:a07.04566981.pdf|A07.pdf}} {{:courses:01tvs:a08.05552637.pdf|A08.pdf}} \\ {{:courses:01tvs:a09.06577702.pdf|A09.pdf}} {{:courses:01tvs:a10.tse_chord_final.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 [[http://www.uppaal.org/|Uppaal]]) | [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/VariantyNIM.pdf|VariantyNIM.pdf]]\\ [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/UPPAAL/uppaal_cviceni.ppsx|uppaal_cviceni.ppsx]]\\ [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/UPPAAL/uppaal_cviceni.pdf|uppaal_cviceni.pdf]]\\ [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/UPPAAL/hra_nim.q|hra_nim.q]]\\ [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/UPPAAL/hra_nim.xml|hra_nim.xml]]\\ [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/UPPAAL/Biphase_Mark_Protocol.xml|Biphase_Mark_Protocol.xml]]\\ [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/UPPAAL/Biphase_Mark_Protocol.q|Biphase_Mark_Protocol.q]] \\ {{:courses:01tvs:seminars:u01.dimacs95.pdf|}} \\ {{:courses:01tvs:seminars:u02.v3i9-0466.pdf|}} \\ {{:courses:01tvs:seminars:u03.10.1007_s00165-006-0008-1.pdf|}} \\ {{:courses:01tvs:seminars:u04.lpw-tacas98.pdf|}} \\ {{:courses:01tvs:seminars:u05.bo-case.pdf|}} \\ {{:courses:01tvs:u06.cs1.pdf|}} \\ {{:courses:01tvs:seminars:u07.fokkink.pdf|}} \\ {{:courses:01tvs:u08.w115.pdf|}} \\ {{:courses:01tvs:u10.fates03.pdf|}} \\ {{:courses:01tvs:seminars:u11.10.1007_978-3-642-16558-0_47.pdf|}} \\ {{:courses:01tvs:seminars:u12.msu-cse-13-7.ps|}} \\ {{:courses:01tvs: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ů| | ===== Podmínky zápočtu ===== * Odevzdání úloh ze všech cvičení. * Docházka na cvičení je povinná. Absence je povolena pouze v dobře zdůvodněných případech. Více než 3 omluvené absence je nutné řešit žádostí a zadáním speciální úlohy. * Za každou odevzdanou úlohu lze získat maximální počet bodů dle tabulky výše. 25% bodů z úlohy je věnováno hodnocení typografické úpravy zprávy (klíčová je čitelnost a přehlednost, nikoliv zdobení). * **Pozdní odevzdávání úloh:** řešení odevzdaná pozdě //mohou// být penalizována 2 až 4 body za každý započatý týden zpoždění (podrobnosti viz Upload system). * Získané body z řešení úloh ze semestru tvoří 40% celkového hodnocení – celkem 100 bodů i se zkouškou. ===== Výsledná známka u zkoušky ===== * Zkouška se skládá ze dvou částí písemných a jedné ústní. Každá písemka trvá 1 hodinu. * **První písemka** obsahuje 2 příklady, které jsou zjednodušené náhodné modifikace variant úloh řešených na seminářích. Pro řešení příkladů je možné použít přinesené přípravy a notebooků. Je možné přistupovat na internet. Není však povoleno s kýmkoliv komunikovat. Za řešení každé úlohy je možné získat maximálně 12 bodů. Celkové body, tj. maximálně 24 bodů, se započítává do hodnocení zkoušky. * V současné době neposkytujeme ukázkové zkušební příklady. * **Druhá písemka** obsahuje 4 otázky dle vypsaných tématických okruhů. Tuto písemku je možné vypracovat pomocí pouze papíru, pera, tužky a své hlavy. Další pomůcky nejsou povoleny. Za každou odpověď je možné získat maximálně 6 bodů. Celkové body, tj. maximálně 24 bodů, se započítává do hodnocení zkoušky. * Body z řešení úloh (s vyjímkou bonusů) ze semestru tvoří maximálně 40% získaných bodů z předmětu, tj. získané body ze semestru se přenáší 1:1 do výsledného bodování při zkoušce. * Dalších maximálně 12 bodů lze udělit za obhájení písemných prací či odpovědi při dodatečných otázkách v rámci ústního zkoušení. Jinak řečeno, ústní zkouška se provádí za účelem prokázat, že student problematice rozumí a ne jenom mechanicky aplikuje postupy. * Výsledná známka ze zkoušky je udělena dle platné stupnice ČVUT vzhledem k maximálnímu počtu 100 bodů. * Ze semestru za řešení úloh je potřeba ziskat minimálně 20 bodů (50%), rovněž součet bodů za písemky musí být minimálně 24 bodů (50%). K absolvování zkoušky je potřeba celkově získat minimálně 50 bodů (50% dle předpisu ČVUT). ČVUT hodnotící tabulka: ^ Body | >=90 | <80, 90) | <70, 80) | <60, 70) | <50, 60) | (0, 50) | ^ Známka | A | B | C | D | E | F |