|
Vyučující
|
-
Barilla Jiří, doc. Ing. Mgr. CSc.
|
|
Obsah předmětu
|
1 Základní informace ke studiu předmětu, podmínky, pravidla. Historie předmětu a základní pojmy. 2 Vybrané partie s teorie množin a výrokové logiky. 3 Formální metody Event-B. 4 Vysvětlení metodiky na příkladu řízení aut na mostě. 5 Matematický zápis modelu řízení aut na mostě a jeho řešení. 6 Analýza příkladu na regulátor mechanického lisu. 7 Matematický zápis modelu regulátoru mechanického lisu a jeho řešení. 8 Jednoduchý protokol pro přenos souborů. 9 Formální zápis modelů Event-B a povinná důkazová pravidla. 10 Ohraničený přenosový protokol. 11 Matematický jazyk Event-B. 12 Synchronizace stromové sítě. 13 Vývoj sekvenčního programu
|
|
Studijní aktivity a metody výuky
|
|
nespecifikováno
|
|
Výstupy z učení
|
Předmět je koncipován jako úvod do modelování v Event-B. Event-B je formální metoda pro modelování a analýzu složitých systémů. Pro formální zápis využívá teorii množin. Modely se vytvářejí postupně od nejjednoduššího k složitějším a při přechodu na další stupeň je model zpřesňován a dochází k jeho verifikaci pomocí matematického důkazu. Tento kurz vznikl v rámci projektu CZ.1.07/2.2.00/28.0296 "Mezioborové vazby a podpora praxe v přírodovědných a technických studijních programech UJEP"
Zvládnutí základů teorie a schopnost aplikace na jednoduché praktické úlohy.
|
|
Předpoklady
|
nespecifikováno
|
|
Hodnoticí metody a kritéria
|
nespecifikováno
75% aktivní účast na cvičeních + vypracování seminární práce a její obhajoba
|
|
Doporučená literatura
|
|