====== A4M33TVS: Testování a verifikace software ====== * [[courses:a4m33tvs:cviceni:state-machine:start|Témata úloh]] (Testování stavového automatu, Model checking) * [[http://cw.felk.cvut.cz/upload/|Odevzdávání úloh]] * [[http://www.feld.cvut.cz/cz/education/rozvrhy-ng/public/cz/predmety/12/58/p12588404.html|Rozvrh]] * [[http://cascade.frozen-doe.net/zp/|Nabídka témat bakalářských a diplomových prací]] ===== 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 | 06.10.2016 | RM | Úvod do testování a verifikace SW. | {{:courses:a4m33tvs:prednasky:01.uvod.pdf|01.uvod.pdf}}{{:courses:a4m33tvs:prednasky:tvsotazky.pdf|}} | | 2 | 13.10.2016 | RM | Optimalizace testovacích sad. | {{:courses:a4m33tvs:prednasky:02.optimalizace.pdf|02.optimalizace.pdf}} | | 3 | 20.10.2016 | RM | Strukturované testování. | {{:courses:a4m33tvs:prednasky:04.strukturovanetestovani.pdf|04.strukturovanetestovani.pdf}} | | 4 | 27.10.2016 | RM | Testování stavových automatů. | {{:courses:a4m33tvs:prednasky:06.konecneautomaty.pdf|06.konecneautomaty.pdf}} \\ {{:courses:a4m33tvs:prednasky:chapter-3.ppt|chapter-3.ppt}} | | 5 | 03.11.2016 | RM | Specifikační jazyky - Alloy | {{:courses:a4m33tvs:prednasky:05.alloy.pdf| 05.alloy.pdf}} | | 6 | 10.11.2016 | RM | Softwarové chyby, kategorizace chyb. \\ Tradiční metody testování. | {{:courses:a4m33tvs:prednasky:03.softwarovechyby.pdf|03.softwarovechyby.pdf}} | | 7 | 17.11.2016 | //(státní svátek)// ||| | 8 | 24.11.2016 | Vyskočil | Verifikace metodou model checking I | {{:courses:a4m33tvs:prednasky:07.modelchecking1.pdf|07.modelchecking1.pdf}} | | 9 | 01.12.2016 | Vyskočil | Verifikace metodou model checking II \\ Temporální logiky | {{:courses:a4m33tvs:prednasky:08.temporalnilogika.pdf|08.temporalnilogika.pdf}} | | 10 | 08.12.2016 | RM? | Verifikace metodou model checking III | {{:courses:a4m33tvs:prednasky:09.modelchecking3.pdf|}} | | 11 | 15.12.2016 | RM | JPF – generování testovacích případů | {{:courses:a4m33tvs:prednasky:11.javapathfinder.pdf|}} | | 12 | 22.12.2016 | RM | Formální metody - Z notace. \\ Formální metody - PVS. | {{:courses:a4m33tvs:prednasky:10.formalnimetodyz.pdf|10.formalnimetodyz.pdf}} \\ {{:courses:a4m33tvs:prednasky:11.formalnimetodypvs.pdf|11.formalnimetodypvs.pdf}}| | 13 | 05.01.2017 | RM | Testování objektově-orientovaného softwaru. | {{:courses:a4m33tvs:prednasky:12.ootestovani.pdf|12.ootestovani.pdf}} | | 14 | 12.01.2017 | RM | Hodnocení spolehlivosti softwaru. \\ Statistické testování | {{:courses:a4m33tvs:prednasky:13.spolehlivost.pdf|13.spolehlivost.pdf}} \\ {{:courses:a4m33tvs:prednasky:13.statisticketestovani.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 [[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 | 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ů. |{{:courses:a4m33tvs:cviceni:ulohyoptimalizace.pdf|UlohyOptimalizace.pdf}} | | 3 | 20.10.2016 | RM,RM | 4 | Vytváření testů pro řídicí tok. | [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/sttCfgUlohy.pdf|sttCfgUlohy.pdf]] | | 4 | 27.10.2016 | RM,RM | 4 | Vytváření testů pro datový tok. | [[http://labe.felk.cvut.cz/~marikr/teaching/A4M33TVS_13/sttDfgUlohy.pdf|sttDfgUlohy.pdf]] | | 5 | 03.11.2016 | RM,RM | 8 | Alloy | {{:courses:a4m33tvs:cviceni: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.)) | | 6 | 10.11.2016 | JK,JK | 8\\ -- | Testování stavového automatu – I. \\ Výběr téma semestrální práce | [[courses:a4m33tvs:cviceni:state-machine:start]] \\ [[https://dip.felk.cvut.cz/browse/pdfcache/severzde_2012dipl.pdf|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 [[http://www.uppaal.org/|Uppaal]])\\ Zadání semestrální práce | [[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]] | | 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 ===== * 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í). * 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. ** 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).