Detail předmětu
Analýza systémů založená na modelech
FIT-MBAAk. rok: 2019/2020
Představení model-based designu, testování, analýzy a model
checkingu. Petriho sítě jako model pro popis paralelních systémů.
Možnosti analýzy Petriho sítí. Markovovy řetězce jako model
pravděpodobnostních systémů. Možnosti analýzy Markovových
řetězců. Časované automaty jako model systémů pracujících s
reálným časem. Možnosti analýzy časovaných automatů. UML a SysML diagramy v rámci model based designu a možnosti
jejich analýzy. Představení nástrojů pro analýzu zmíněných
modelů.
Garant předmětu
Zajišťuje ústav
Prerekvizity
Základní znalosti z teorie grafů, formálních jazyků a automatů. Základní znalost pojmů statistiky a pravděpodobnosti. Základní znalosti softwarového inženýrství.
- doporučená prerekvizita
Doporučená nebo povinná literatura
Jensen, K.: Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, Springer Verlag, 1993. ISBN: 3-540-60943-1
Kaynar, D., Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010. ISBN-13: 978-1608450022 Dostupné online.
Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640 Dostupné online (https://link.springer.com/book/10.1007%2F978-3-319-47766-4) ze sítě VUT.
Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, MIT Press, 2008. ISBN: 978-0-262-02649-9
Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0-387-13723-8
Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8-085-86735-4
Kaynar, D., Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010. ISBN-13: 978-1608450022
Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640
Jazyk výuky
čeština
Cíl
Seznámit studenty s možností zajištění kvality software (event.
hardware) formou vytvoření modelu, ověření správnosti na úrovni
modelu a následné (někdy i automatizovaná) konverze modelu do
cílového programovacího jazyka. Tyto principy budou představeny
na čtyřech modelovacích technikách: Petriho sítích, Markovových
řetězcích, časovaných automatech a UML/SysML diagramech.
Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky
3 projekty po 10 bodech.
Pro získání bodů ze závěrečné semestrální zkoušky
je nutné tuto zkoušku složit tak, aby byla hodnocena nejméně 30 body. V opačném
případě bude zkouška hodnocena 0 body.
Zařazení předmětu ve studijních plánech
- Program IT-MGR-2 magisterský navazující
obor MBS , libovolný ročník, letní semestr, 5 kreditů, volitelný
obor MBI , libovolný ročník, letní semestr, 5 kreditů, volitelný
obor MMM , libovolný ročník, letní semestr, 5 kreditů, povinný
obor MPV , libovolný ročník, letní semestr, 5 kreditů, volitelný
obor MSK , libovolný ročník, letní semestr, 5 kreditů, volitelný - Program MITAI magisterský navazující
specializace NBIO , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NISD , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NISY , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NIDE , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NCPS , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NSEC , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NMAT , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NGRI , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NNET , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NVIZ , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NSEN , libovolný ročník, letní semestr, 5 kreditů, povinný
specializace NMAL , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NHPC , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NVER , libovolný ročník, letní semestr, 5 kreditů, povinný
specializace NEMB , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NADE , libovolný ročník, letní semestr, 5 kreditů, volitelný
specializace NSPE , libovolný ročník, letní semestr, 5 kreditů, volitelný - Program IT-MGR-2 magisterský navazující
obor MIS , 2. ročník, letní semestr, 5 kreditů, povinně volitelný
obor MIN , 2. ročník, letní semestr, 5 kreditů, povinný
obor MGM , 2. ročník, letní semestr, 5 kreditů, volitelný
Typ (způsob) výuky
Přednáška
39 hod., nepovinná
Vyučující / Lektor
Osnova
Úvod do
problematiky model-based designu, testování a analýzy. Pojem
model-checking.
Petriho sítě.
Základní pojmy, historie a aplikace.
P/T Petriho
sítě, definice, evoluční pravidla, stavový prostor, základní
problémy analýzy (bezpečnost, omezenost, konzervativnost,
živost).
Analýza P/T
Petriho sítí, strom dosažitelných značení, P- a T- invarianty.
Rozšíření
P/T Petriho sítí a Barvené sítě. Rozhodnutelnost a vztah k
Turingovým strojům. Ukázka nástrojů NetLab a PIPE.
Využití
Markovových řetězců k modelování pravděpodobnostních
systémů, Markovovy řetězce v diskrétním a spojitém čase.
Temporální logika pro specifikaci chování Markovových řetězců
Analýza
Markovových řetězců (model checking), Ukázka nástroje PRISM.
Rozšíření
Markovových řetězců o nedeterminismus - Markovovy rozhodovací
procesy. Využití Markovových rozhodovací procesů v teorii
řízení. Syntéza řízení pro Markovovy rozhodovací procesy.
Časované
automaty a jejich využití pro modelování systémů s reálným
časem.
Analýza
časovaných automatů, abstrakce založená na regionech,
rozhodnutelné problémy. Ukázka nástroje UPPAAL.
Časovaná
temporální logika TCTL a její vztah k časovaným automatům
UML/SysML
diagramy a jejich využití v rámci model-based designu a analýzy.
- Model
checking systémů popsaných pomocí UML (stavových) diagramů.
Cvičení na počítači
6 hod., povinná
Vyučující / Lektor
Osnova
Pokud budou cvičení, tak osnova bude následující:
- Analýza P/T Petriho sítí, ukázka nástrojů NetLab a PIPE.
- Analýza Markovových řetězců, ukázka nástroje PRISM
- Analýza časovaných automatů, ukázka nástroje UPPAAL.
Projekt
7 hod., povinná
Vyučující / Lektor
Osnova
1. Aplikace Petriho sítí.
2. Aplikace Markovových řetězců.
3. Aplikace časovaných automatů.