Detail předmětu

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

MBA Ak. rok 2023/2024 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í

  • 60 bodů závěrečná zkouška (písemná část)
  • 40 bodů projekty

Zajišťuje ústav

Přednášející

Cvičící

Stránky předmětu

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.

Proč je předmět vyučován

Klasickým přístupem k vývoji software je jeho implementace ve vybraném programovacím jazyce a následné testování, eventuálně verifikace. V rámci zajištění kvality embeded a safety-critical systémů se ale často využívá přístup, kdy nejprve vytvoříme model (části) systému ve vhodném modelovacím jazyce a následně provedeme ověření kvality na úrovni modelu. Teprve poté provedeme (často automatizovanou) konverzi modelu do cílového programovacího jazyka. Ověření vlastností na úrovni modelu je často mnohem jednodušší než ověření stejných vlastností na úrovni zdrojových kódů.

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

Osnova počítačových cvičení

  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é)

Osnova ostatní - projekty, práce

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

 

 

Průběžná kontrola studia

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.

Rozvrh

DenTypTýdnyMístn.OdDoKapacitaPSKSkupInfo
Po poč. lab 5., 7. výuky N203 16:0017:5020 1MIT 2MIT xx Rogalewicz
Po poč. lab 10., 11. výuky N203 16:0017:5020 1MIT 2MIT xx Andriushchenko
Po poč. lab 2024-04-22 N203 16:0017:5020 1MIT 2MIT xx
Po poč. lab 2024-04-29 N203 16:0017:5020 1MIT 2MIT xx Fiedor
Út přednáška 1., 2., 4., 5., 6., 7. výuky D0206 10:0011:50154 1MIT 2MIT NIDE NMAT NSEN NVER xx Rogalewicz
Út přednáška 8., 9., 10. výuky D0206 10:0011:50154 1MIT 2MIT NIDE NMAT NSEN NVER xx Češka
Út přednáška 11., 12., 13. výuky D0206 10:0011:50154 1MIT 2MIT NIDE NMAT NSEN NVER xx Fiedor
Út přednáška 2024-02-20 D0206 10:0011:50154 1MIT 2MIT NIDE NMAT NSEN NVER xx Holík

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

Nahoru