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

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

Kaynar, D.,  Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010.  ISBN-13: 978-1608450022 Dostupné online.
Č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

Elearning

Zařazení předmětu ve studijních plánech

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

    obor MIS , 2 ročník, letní semestr, povinně volitelný
    obor MBS , 0 ročník, letní semestr, volitelný
    obor MPV , 0 ročník, letní semestr, volitelný
    obor MIN , 2 ročník, letní semestr, povinný
    obor MGM , 2 ročník, letní semestr, volitelný
    obor MBI , 0 ročník, letní semestr, volitelný
    obor MSK , 0 ročník, letní semestr, volitelný
    obor MMM , 0 ročník, letní semestr, povinný

  • Program MITAI magisterský navazující

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

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

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

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

Osnova

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

 

 

Elearning