IV101 Seminář z verifikace

Fakulta informatiky
jaro 2013
Rozsah
0/2. 2 kr. 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
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Po 13:00–14:50 B411
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 12 stud.
Momentální stav registrace a zápisu: zapsáno: 0/12, pouze zareg.: 0/12, pouze zareg. s předností (mateřské obory): 0/12
Mateřské obory/plány
předmět má 37 mateřských oborů, zobrazit
Anotace
Cílem semináře je získání praktických dovedností a zkušeností s automatizovanou verifikací počítačových systémů. Konkrétně by studenti po absolvování tohoto kurzu měli být schopni smysluplně použít většinu standardních nástrojů pro ověřování modelu, jako jsou DiVinE, SPIN, UPPAAL, nebo PRISM.
Klíčová témata
V rámci semináře se studenti seznámí s několika nejpoužívanějšími verifikačními nástroji, vhodnými formalizmy pro vyjádření vlastností systémů a vypracují verifikační projekt v rozsahu 15 hod.
Studijní zdroje a literatura
  • Peled, Doron. Software Reliability Methods. Springer, 2001.
  • HOLZMANN, Gerald J. The spin model checker :primer and reference manual. Boston: Addison-Wesley, 2004, xii, 596 s. ISBN 0-321-22862-6. info
  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Přístupy, postupy a metody používané ve výuce
teoretická příprava, práce na projektu
Způsob ověření výstupů z učení a požadavky na ukončení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Odkaz a informace vyučujících
http://www.fi.muni.cz/~xbarnat/IV101/
Další komentáře
Studijní materiály
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2003, jaro 2004, podzim 2004, jaro 2005, podzim 2005, jaro 2007, jaro 2008, jaro 2009, jaro 2010, jaro 2012, jaro 2015.