Detail předmětu

Analýza systémů založená na modelech

FIT-MBAAk. rok: 2023/2024

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ů.

Jazyk výuky

čeština

Počet kreditů

5

Garant předmětu

doc. Mgr. Adam Rogalewicz, Ph.D.

Zajišťuje ústav

Ústav inteligentních systémů (UITS)

Vstupní znalosti

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í.

Pravidla hodnocení a ukončení předmětu

Bodové hodnocení vypracovaných projektů (max. 40 bodů) a závěrečné semestrální zkoušky (max 60 bodů).


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ě 25 body. V opačném případě bude zkouška hodnocena 0 body.

Učební cíle

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.

Prerekvizity a korekvizity

Základní literatura

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.

Doporučená literatura

Č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.

eLearning

eLearning: aktuální otevřený kurz

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, volitelný
    obor MBI , libovolný ročník, letní semestr, volitelný
    obor MMM , libovolný ročník, letní semestr, povinný
    obor MPV , libovolný ročník, letní semestr, volitelný
    obor MSK , libovolný ročník, letní semestr, volitelný

  • Program MITAI magisterský navazující

    specializace NBIO , libovolný ročník, letní semestr, volitelný
    specializace NISD , libovolný ročník, letní semestr, volitelný
    specializace NISY do 2020/21 , libovolný ročník, letní semestr, volitelný
    specializace NISY , libovolný ročník, letní semestr, volitelný
    specializace NIDE , libovolný ročník, letní semestr, volitelný
    specializace NCPS , libovolný ročník, letní semestr, volitelný
    specializace NSEC , libovolný ročník, letní semestr, volitelný
    specializace NMAT , libovolný ročník, letní semestr, volitelný
    specializace NGRI , libovolný ročník, letní semestr, volitelný
    specializace NNET , libovolný ročník, letní semestr, volitelný
    specializace NVIZ , libovolný ročník, letní semestr, volitelný
    specializace NSEN , libovolný ročník, letní semestr, povinný
    specializace NMAL , libovolný ročník, letní semestr, volitelný
    specializace NHPC , libovolný ročník, letní semestr, volitelný
    specializace NVER , libovolný ročník, letní semestr, povinný
    specializace NEMB , libovolný ročník, letní semestr, volitelný
    specializace NEMB do 2021/22 , libovolný ročník, letní semestr, volitelný
    specializace NADE , libovolný ročník, letní semestr, volitelný
    specializace NSPE , libovolný ročník, letní semestr, volitelný

  • Program IT-MGR-2 magisterský navazující

    obor MIS , 2. ročník, letní semestr, povinně volitelný
    obor MIN , 2. ročník, letní semestr, povinný
    obor MGM , 2. ročník, letní semestr, volitelný

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

doc. RNDr. Milan Češka, Ph.D.
Ing. Jan Fiedor, Ph.D.
doc. Mgr. Lukáš Holík, Ph.D.
doc. Mgr. Adam Rogalewicz, Ph.D.

Osnova

  1. Úvod do problematiky model-based designu, testování a analýzy. Pojem model-checking.
  2. P/T Petriho sítě, definice, evoluční pravidla, stavový prostor, základní problémy analýzy, P- a T- invarianty.
  3. Analýza P/T Petriho sítí, strom dosažitelných značení, zpětná analýza.
  4. Jazyky a rozšíření P/T Petriho sítí, Barvené sítě. Rozhodnutelnost a vztah k Turingovým strojům.
  5. 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ů
  6. Analýza Markovových řetězců (model checking).
  7. 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.
  8. Časované automaty a jejich využití pro modelování systémů s reálným časem, abstrakce založená na regionech.
  9. Časovaná temporální logika TCTL a její vztah k časovaným automatům
  10. Rozhodnutelné problémy pro časované automaty, simulace a bisimulace.
  11. UML/SysML diagramy a jejich využití v rámci model-based designu a analýzy.
  12. Model checking systémů popsaných pomocí UML (stavových) diagramů.
  13. Mathlab-Simulink, principy modelování

Cvičení na počítači

10 hod., povinná

Vyučující / Lektor

Ing. Roman Andriushchenko
Ing. Jan Fiedor, Ph.D.
doc. Mgr. Lukáš Holík, Ph.D.
doc. Mgr. Adam Rogalewicz, Ph.D.

Osnova

  1. Analýza P/T Petriho sítí, nástroj NetLab (K)
  2. Výpočty nad Markovovými řetězci (N)
  3. Modelování v nástroji PRISM. (P)
  4. Analýza časovaných automatů, nástroj UPPAAL. (K)
  5. Modelování v Mathlab-simulink (P)

(P – počítačové, N – numerické, K - kombinované)

Projekt

16 hod., povinná

Vyučující / Lektor

Ing. Roman Andriushchenko
Ing. Jan Fiedor, Ph.D.
doc. Mgr. Lukáš Holík, Ph.D.
doc. Mgr. Adam Rogalewicz, Ph.D.

Osnova

  1. Aplikace Petriho sítí.
  2. Aplikace Markovových řetězců.
  3. Aplikace časovaných automatů.
  4. Modelování v Mathlab-Simulink

 

 

eLearning

eLearning: aktuální otevřený kurz