IV113 Úvod do validace a verifikace

Fakulta informatiky
podzim 2018
Rozsah
2/0/0. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
Vyučující
prof. RNDr. Jiří Barnat, Ph.D. (přednášející)
Garance
prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Jiří Barnat, Ph.D.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
St 16:00–17:50 B411
Předpoklady
(! IA169 System Verif. and Assurance ) && (!NOW( IA169 System Verif. and Assurance ))
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 47 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je orientovat studenty v základních přístupech k validaci a verifikaci počítačových programů.
Výstupy z učení
Po úspěšném absolvování předmětu by studenti měli být schopni rozhodnout o vhodnosti validačních a verifikačních technik použitých během vývoje softwarového produktu, měli by být schopni formulovat vlastnosti systémů v temporálních logikách, měli by rozumnět způsobu, kterým lze tyto vlastnosti verifikovat pomocí nástrojů pro ověřování modelu, a měli by chápat principy, na kterých tyto nástroje fungují.
Osnova
  • Úvodní přehled technik pro validaci a verifikaci. Mise testování, strategie testování, problém orákula, doménové testování, regresní testování. Symbolická exekuce. Deduktivní verifikace. LTL model checking, CTL model checking, techniky redukce stavového prostoru. Bounded model checking. Úvod do analýzy programů.
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • http://www.testingeducation.org/BBST/index.html
  • BAIER, Christel a Joost-Pieter KATOEN. Principles of model checking. Cambridge, Mass.: MIT Press, 2008, xvii, 975. ISBN 9780262026499. info
Výukové metody
Teoretická příprava, domácí úkoly.
Metody hodnocení
Předmět je zakončen ústní zkouškou na odpřednášenou látku. Nepovinná účast na přednáškách. Pro zakončení stupněm A je navíc nutné vypracovat domácí úlohy zadané na přednáškách.
Navazující předměty
Informace učitele
http://www.fi.muni.cz/~xbarnat/IV113/index.html
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017.
  • Statistika zápisu (nejnovější)
  • Permalink: https://is.muni.cz/predmet/fi/podzim2018/IV113