Detail předmětu
Analýza systémů založená na modelech
MBA Ak. rok 2024/2025 letní semestr 5 kreditů
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
Koordinátor předmětu
Jazyk výuky
Zakončení
Rozsah
- 26 hod. přednášky
- 10 hod. pc laboratoře
- 16 hod. projekty
Bodové hodnocení
- 70 bodů závěrečná zkouška
- 30 bodů projekty
Zajišťuje ústav
Přednášející
Fiedor Jan, Ing., Ph.D. (UITS)
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Cvičící
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Cíle předmětu
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.
Doporučené prerekvizity
- Teoretická informatika (TIN)
Požadované prerekvizitní znalosti a dovednosti
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í.
Literatura studijní
- Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8-085-86735-4
- 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.
Literatura referenční
- 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
- Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer, 2017. ISBN-13: 978-3319477640 Dostupné online ze sítě VUT.
Osnova přednášek
- Ú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ů.
Osnova počítačových cvičení
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.
Osnova ostatní - projekty, práce
1. Aplikace Petriho sítí.
2. Aplikace Markovových řetězců.
3. Aplikace časovaných automatů.
Průběžná kontrola studia
Bodové hodnocení vypracovaných projektů (max. 30 bodů) a závěrečné semestrální zkoušky (max 70 bodů).
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.
Rozvrh
Den | Typ | Týdny | Místn. | Od | Do | Kapacita | PSK | Skup | Info |
---|---|---|---|---|---|---|---|---|---|
Po | poč. lab | výuky | N203 | 16:00 | 17:50 | 20 | 1MIT 2MIT | xx | |
Út | přednáška | 1., 2., 4., 5., 6., 7. výuky | D0207 | 10:00 | 11:50 | 90 | 1MIT 2MIT | NSEN NVER xx | Rogalewicz |
Út | přednáška | 8., 9., 10. výuky | D0207 | 10:00 | 11:50 | 90 | 1MIT 2MIT | NSEN NVER xx | Češka |
Út | přednáška | 11., 12., 13. výuky | D0207 | 10:00 | 11:50 | 90 | 1MIT 2MIT | NSEN NVER xx | Fiedor |
Út | přednáška | 2025-02-25 | D0207 | 10:00 | 11:50 | 90 | 1MIT 2MIT | NSEN NVER xx | Holík |
Pá | poč. lab | výuky | N105 | 13:00 | 14:50 | 20 | 1MIT 2MIT | xx |
Zařazení předmětu ve studijních plánech