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
Cíle předmětu
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.
Osnova
  • 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.
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
Výukové metody
teoretická příprava, práce na projektu
Metody hodnocení
Studenti jsou hodnoceni na základě samostatné práce na projektech.
Informace učitele
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.