FI:IV101 Seminář z verifikace - Informace o předmětu

IV101 Seminář z verifikace

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

• Aplikovaná informatika (program FI, B-AP)
• Aplikovaná informatika (program FI, N-AP)
• Bezpečnost informačních technologií (program FI, N-IN)
• Bioinformatika (program FI, B-AP)
• Bioinformatika (program FI, N-AP)
• Informační systémy (program FI, N-IN)
• Informatika a druhý obor (program FI, B-BI)
• Informatika a druhý obor (program FI, B-EB)
• Informatika a druhý obor (program FI, B-FY)
• Informatika a druhý obor (program FI, B-GE)
• Informatika a druhý obor (program FI, B-GK)
• Informatika a druhý obor (program FI, B-CH)
• Informatika a druhý obor (program FI, B-IO)
• Informatika a druhý obor (program FI, B-MA)
• Informatika a druhý obor (program FI, B-TV)
• Informatika (program FI, N-IN)
• Matematická informatika (program FI, B-IN)
• Paralelní a distribuované systémy (program FI, B-IN)
• Paralelní a distribuované systémy (program FI, N-IN)
• Počítačová grafika a zpracování obrazu (program FI, B-IN)
• Počítačová grafika (program FI, N-IN)
• Počítačové sítě a komunikace (program FI, B-IN)
• Počítačové sítě a komunikace (program FI, N-IN)
• Počítačové systémy a zpracování dat (program FI, B-IN)
• Počítačové systémy (program FI, N-IN)
• Programovatelné technické struktury (angl.) (program FI, N-IN)
• Programovatelné technické struktury (program FI, B-IN)
• Programovatelné technické struktury (program FI, N-IN)
• Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
• Služby - výzkum, řízení a inovace (program FI, N-AP)
• Sociální informatika (program FI, B-AP)
• Teoretická informatika (program FI, N-IN)
• Učitelství výpočetní techniky pro střední školy (program FI, N-SS) (2)
• Umělá inteligence a zpracování přirozeného jazyka (program FI, B-IN)
• Umělá inteligence a zpracování přirozeného jazyka (program FI, N-IN)
• Zpracování obrazu (program FI, N-AP)

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.

• Statistika zápisu (jaro 2013, nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/jaro2013/IV101