IV113 Úvod do validace a verifikace

Fakulta informatiky
podzim 2008
Rozsah
2/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.
Rozvrh
Čt 16:00–17:50 B011
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á 37 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je seznámit studenty se základními technikami validace a verifikace počítačových systémů. 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, jak 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í. Formální verifikace sekvenčních a paralelních programů, LTL model checking, CTL model checking, techniky redukce stavového prostoru.
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
Metody hodnocení
Ukončení písemnou zkouškou na odpřednášenou látku. Nepovinné přednášky, bez domácích úloh.
Navazující předměty
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích podzim 2007, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018.