Hlavní stránka | Seznam oborů/specializací | Seznam všech skupin předmětů | Seznam všech předmětů | Seznam rolí                Návod

Předmět je základní jednotka výuky, jejímž prostřednictvím si student osvojí ucelenou část souboru znalostí a dovedností, potřebnou pro zvládnutí studijního oboru/specializace. Za věcný obsah předmětu zodpovídá garant předmětu. Časovou náročnost předmětu zhruba vyjadřuje atribut předmětu rozsah kontaktní výuky. Například rozsah = 2+2  značí, že předmět bude mít týdně dvě hodiny přednášek a dvě hodiny cvičení týdně. Na závěr semestru musí vyučující provést vyhodnocení, nakolik si ten který student osvojil poznatky a dovednosti, kterých měl během výuky nabýt. Jakým způsobem toto hodnocení vyučující provedou určuje atribut způsob zakončení. U předmětu lze definovat, že předmět je zakončen pouze zápočtem(Z), klasifikovaným zápočtem(KZ), pouze zkouškou(ZK), nebo zápočtem a zkouškou(Z,ZK). Náročnost úspěšného absolvování předmětu je vyjádřena ECTS kreditními body. Výuka předmětu probíhá během semestru. Opakovaně se předmět vyučuje vždy v zimním(Z), nebo v letním(L) semestru každého akademického roku. Výjimečně může předmět být nabízen studentům v obou semestrech(Z,L). Za organizační zajištění výuky zodpovídá přiřazená katedra, která zejména vytvoří časový rozvrh předmětu a zajistí pro předmět vyučující. Někteří přednáší a zkouší, jiní vedou cvičení a udělují zápočty.
Obsahová náplň a další organizační informace, týkající se předmětu je popsána pomocí různých popisných textů(anotace, týdenní osnova, literatura, apod.)
$DODATEK_POPIS
MI-FME.16 Formální metody a specifikace Rozsah kontaktní výuky: 2P+1C
Vyučující: Způsob zakončení: Z,ZK
Zodpovědná katedra: 18102 ECTS Kredity: 5 Semestr: L

Anotace:
Studenti dokážou formálně popisovat sémantiku software a používat logické uvažování pro konstrukci správně fungujícího software. Naučí se použít některé programové nástroje, které slouží pro dokazování vlastností softwaru.

Osnovy přednášek:
1. Specifikace programů a základy praktické logiky
2. Logické teorie a modelování datových struktur
3. Operační sémantika programů
4. Omezená správnost programů
5. Ověření neomezené správnosti programů
6. Terminace, totální správnost programů
7. Symbolické provádění programů

Osnovy cvičení:
Cvičení materiálu z přednášky.

Literatura:
Aaron R. Bradley and Zohar Manna: ''The Calculus of Computation'', Springer Verlag, 2007 Edmund M. Clarke, Orna Grumberg, and Doron A. Peled: ''Model Checking'', MIT Press, 1999 Zohar Manna and Amir Pnueli: ''Temporal Verification of Reactive Systems'', Springer Verlag, 1995

Požadavky:
Znalost základních pojmů matematické logiky a teorie množin, schopnost je používat.

Informace o předmětu a výukové materiály naleznete na https://moodle-vyuka.cvut.cz/course/view.php?id=2728

Předmět je zahrnut do těchto studijních plánů:
Plán Obor Role Dop. semestr
MI-WSI-WI.2016 Webové a softwarové inženýrství V 2
MI-WSI-SI.2016 Webové a softwarové inženýrství PZ 2
MI-WSI-ISM.2016 Webové a softwarové inženýrství V 2
MI-PB.2016 Počítačová bezpečnost V 2
MI-SP-SP.2016 Systémové programování V 2
MI-ZI.2016 Znalostní inženýrství V 2
MI-ZI.2018 Znalostní inženýrství V 2
NI-TI.2018 Teoretická informatika V 2
MI-SPOL.2016 Nespecifikovaný/á obor/specializace studia - Unspecified Branch/Specialisation of Study VO 2
MI-SP-TI.2016 Systémové programování V 2
MI-NPVS.2016 Návrh a programování vestavných systémů V 2
MI-PSS.2016 Počítačové systémy a sítě V 2


Stránka vytvořena 28. 3. 2024, semestry: Z/2022-3, L/2020-1, L/2019-20, L/2023-4, L/2022-3, Z/2023-4, Z/2019-20, Z/2021-2, Z/2020-1, L/2021-2, připomínky k informační náplni zasílejte správci studijních plánů Návrh a realizace: J. Novák, I. Halaška