Název:

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

Zkratka:MBA
Ak.rok:2019/2020
Semestr:letní
Studijní plán:
ProgramObor/
specializace
RočníkPovinnost
IT-MGR-2MBI-volitelný
IT-MGR-2MBS-volitelný
IT-MGR-2MGM2.volitelný
IT-MGR-2MIN2.povinný
IT-MGR-2MIS2.povinně volitelný - skupina F
IT-MGR-2MMM-povinný
IT-MGR-2MPV-volitelný
IT-MGR-2MSK-volitelný
MITAINADE-volitelný
MITAINBIO-volitelný
MITAINCPS-volitelný
MITAINEMB-volitelný
MITAINGRI-volitelný
MITAINHPC-volitelný
MITAINIDE-volitelný
MITAINISD-volitelný
MITAINISY-volitelný
MITAINMAL-volitelný
MITAINMAT-volitelný
MITAINNET-volitelný
MITAINSEC-volitelný
MITAINSEN-povinný
MITAINSPE-volitelný
MITAINVER-povinný
MITAINVIZ-volitelný
Vyučovací jazyk:čeština
Kredity:5 kreditů
Ukončení:zkouška (kombinovaná)
Výuka:
hod./sempřednáškasem./cvič.lab. cvič.poč. cvič.jiná
Rozsah:390067
 zkouškatestycvičenílaboratořeostatní
Body:7000030
Garant:Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Zástupce garanta:Češka Milan, prof. RNDr., CSc. (UITS)
Přednášející:Češka Milan, RNDr., Ph.D. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav inteligentních systémů FIT VUT v Brně
Prerekvizity: 
Teoretická informatika (TIN), UITS
Rozvrh:
DenVýukaTýdenMístnostOdDoPSKSkupiny
ÚtpřednáškavýukyA113 17:0019:501MIT 2MIT MIN MMM xx
 
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.
Anotace:
  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ů.
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í.
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ů.
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ů.
Literatura referenční:
 
  • Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0-387-13723-8
  • Češka, M.: Petriho sítě, Akad.nakl. CERM, Brno, 1994. ISBN: 8-085-86735-4
  • Kaynar, D.,  Lynch, N., Segala, R., Vaandrager, F. :The Theory of Timed I/O Automata, Morgan & Claypool, 2010.  ISBN-13: 978-1608450022
  • Boucherie, R. J.(editor), van Dijk, N. M. (editor): Markov Decision Processes in Practice, Springer,  2017.  ISBN-13: 978-3319477640
Literatura studijní:
 
  • Reisig, W.: Petri Nets, An Introduction, Springer Verlag, 1985. ISBN: 0-387-13723-8
  • Č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.
  • 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.
Kontrolovaná výuka:
  3 projekty po 10 bodech.
 

Vaše IPv4 adresa: 54.210.158.163