460-4019/03 – Petriho sítě II (PES II)
Garantující katedra | Katedra informatiky | Kredity | 4 |
Garant předmětu | doc. Ing. Zdeněk Sawa, Ph.D. | Garant verze předmětu | doc. Ing. Zdeněk Sawa, Ph.D. |
Úroveň studia | pregraduální nebo graduální | Povinnost | volitelný odborný |
Ročník | 1 | Semestr | letní |
| | Jazyk výuky | angličtina |
Rok zavedení | 2015/2016 | Rok zrušení | 2022/2023 |
Určeno pro fakulty | FEI | Určeno pro typy studia | navazující magisterské |
Cíle předmětu vyjádřené dosaženými dovednostmi a kompetencemi
Cílem je podat základní informaci o teorii a praktických možnostech Petriho sítí vysoké úrovně (HLPN - High Level Petri Nets) při specifikaci, modelování a analýze složitých distribuovaných systémů s paralelními procesy. Výklad je zaměřen na dnes nejrozšířenější variantu HLPN - barvené Petriho sítě (CPN - Coloured Petri Nets) podle K.Jensena.
Vyučovací metody
Přednášky
Cvičení (v učebně)
Anotace
Přednáška Petriho sítě II (High-level Petri Nets - HLPN) navazuje na přednášku Petriho sítě I (Low-level Petri Nets- LLPN). HLPN, na rozdíl od LLPN, umožňují pracovat s individuálními objekty a jejich třídami (např. daty různě strukturovanými a s jejich hodnotami) a s hierarchickými strukturami (třídami modulů s přesně definovaným rozhraním). Přitom se zachovávají všechny přednosti Petriho sítí (grafická vizualizace, matematická rigoróznost,...). HLPN umožňují integrovat osvědčené (ale teoreticky ne plně zdůvodněné) paradigma objektově orientovaného přístupu s exaktním matematickým aparátem Petriho sítí. HLPN představují jazyk vysoké úrovně pro analýzu, návrh a modelování složitých distribuovaných systémů s paralelními procesy. Tento jazyk má má mnoho aplikací, a to nejenom v informatice.
Povinná literatura:
K.Jensen: Coloured Petri Nets (Basic Concepts), Volume 1, Springer - Verlag, 1992, 1996.
www.informatik.uni-hamburg.de/TGI/PetriNets - Welcome to the Petri Nets World
http://wiki.daimi.au.dk/cpntools/cpntools.wiki Computer Tool for Coloured Petri Nets
http://www.daimi.au.dk/CPnets/ These Web pages present the activities of the CPN group at the Department of Computer Science, University of Aarhus, Denmark
Doporučená literatura:
K.Jensen, G.Rozenberg (Eds.): High-level Petri Nets (Theory and Application). Springer-Verlag, 1991.
K.Jensen (Ed.): Application and Theory of Petri Nets . Springer-Verlag, 1992
R.David, H.Alla: Petri Nets and Grafcet (Tools for modelling discrete event systems). Prentice Hall Ltd., 1992
W.Resig-G.Rozenberg (Eds.): Lectures on Petri Nets I: Basic Models, LNCS 1491, Springer, 1998.
W.Resig-G.Rozenberg (Eds.): Lectures on Petri Nets II: Applications, LNCS 1492, Springer, 1998.
M.A.Marsan, G.Balbo, G.Conte, S.Donatelli, G.Franceschinis: Modelling with Generalised Stochastic Petri Nets. Series in Parallel Computing, John Wiley & Sons, 1995.
K.Jensen: Coloured Petri Nets (Analysis Methods), Volume 2, Springer - Verlag, 1995.
K.Jensen: Coloured Petri Nets (Practical Use), Volume 3, Springer - Verlag, 1997.
Forma způsobu ověření studijních výsledků a další požadavky na studenta
E-learning
Další požadavky na studenta
Další požadavky na studenty nejsou kladeny.
Prerekvizity
Předmět nemá žádné prerekvizity.
Korekvizity
Předmět nemá žádné korekvizity.
Osnova předmětu
Přednášky:
1) Úvod do barevných Petriho sítí
2) Základy jazyka CPN ML
3) Analýza stavového prostoru barevných Petriho sítí
4) Časované barevné sítě
5) Analýza výkonnosti (performance)
6) Hierarchické sítě
7) Formální definice barevných Petriho sítí - základní definice
8) Formální definice barevných Petriho sítí - operační sémantika
9) Další varianty časovaných sítí a nástroj TAPAAL
10) Úvod do lineární temporální logiky (LTL)
11) High-level PN a jejich využití jako programovacího prostředku pro distribuované aplikace
12) Porovnání Petriho sítí s jinými modelovacími prostředky
13) Záverečné shrnutí
Cvičení:
1) Příklady jednoduchých barevných Petriho sítí
2) Příklady základních konstrukcí použivaných v barevných Petriho sítích
3) Příklady pro verifikaci pomocí analýzy stavového prostoru
4) Příklady pro časované sítě
5) Příklady pro performance analýzu časovaných sítí
6) Příklady na hierarchické sítě
7) Příklady na ověření pochopení základních definic barevných Petriho sítí
8) Příklady složitějších systemů modelovaných pomocí barevných Petriho sití
9) Příklad na modelovaní s nástrojem TAAPAL
10) Příklad verifikace pomocí nástroje TAAPAL
11) Příklad na použití nástroje Kaira
12) Diskuse modelů vytvořených studenty
13) Shrnutí, připomenutí procvičení nejtěžších pasáží
Podmínky absolvování předmětu
Výskyt ve studijních plánech
Výskyt ve speciálních blocích
Hodnocení Výuky
Předmět neobsahuje žádné hodnocení.