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

česky

Zakončení

zkouška (kombinovaná)

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í

Cvičící

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

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

  1. Úvod do problematiky model-based designu, testování a analýzy. Pojem model-checking.
  2. Petriho sítě. Základní pojmy, historie a aplikace.
  3. P/T Petriho sítě, definice, evoluční pravidla, stavový prostor, základní problémy analýzy (bezpečnost, omezenost, konzervativnost, živost).
  4. Analýza P/T Petriho sítí, strom dosažitelných značení, P- a T- invarianty.
  5. 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.
  6. 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ů
  7. Analýza Markovových řetězců (model checking), Ukázka nástroje PRISM.
  8. 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.
  9. Časované automaty a jejich využití pro modelování systémů s reálným časem.
  10. Analýza časovaných automatů, abstrakce založená na regionech, rozhodnutelné problémy. Ukázka nástroje UPPAAL.
  11. Časovaná temporální logika TCTL a její vztah k časovaným automatům
  12. UML/SysML diagramy a jejich využití v rámci model-based designu a analýzy.
  13. 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í:

  1. Analýza P/T Petriho sítí, ukázka nástrojů NetLab a PIPE.
  2. Analýza Markovových řetězců, ukázka nástroje PRISM
  3. 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

DenTypTýdnyMístn.OdDoKapacitaPSKSkupInfo
Po poč. lab výuky N203 16:0017:5020 1MIT 2MIT xx
Út přednáška 1., 2., 4., 5., 6., 7. výuky D0207 10:0011:5090 1MIT 2MIT NSEN NVER xx Rogalewicz
Út přednáška 8., 9., 10. výuky D0207 10:0011:5090 1MIT 2MIT NSEN NVER xx Češka
Út přednáška 11., 12., 13. výuky D0207 10:0011:5090 1MIT 2MIT NSEN NVER xx Fiedor
Út přednáška 2025-02-25 D0207 10:0011:5090 1MIT 2MIT NSEN NVER xx Holík
poč. lab výuky N105 13:0014:5020 1MIT 2MIT xx

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

Nahoru