460-4019/02 – Petriho sítě II (PES II)

Garantující katedraKatedra informatikyKredity4
Garant předmětuprof. RNDr. Petr Jančar, CSc.Garant verze předmětuprof. RNDr. Petr Jančar, CSc.
Úroveň studiapregraduální nebo graduálníPovinnostvolitelný odborný
Ročník1Semestrletní
Odkaz na webJazyk výukyčeština
Rok zavedení2015/2016Rok zrušení
Určeno pro fakultyFEIUrčeno pro typy studianavazující magisterské
Výuku zajišťuje
Os. čís.JménoCvičícíPřednášející
JAN59 prof. RNDr. Petr Jančar, CSc.
SUR096 Ing. Martin Šurkovský
Rozsah výuky pro formy studia
Forma studiaZp.zak.Rozsah
prezenční Zápočet a zkouška 2+2
kombinovaná Zápočet a zkouška 10+0

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.

Způsob průběžné kontroly znalostí během semestru

E-learning

Další požadavky na studenta

Další požadavky na studenty nejsou kladeny.

Minimální znalostní požadavky

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

Prezenční forma (platnost od: 2015/2016 zimní semestr)
Název úlohyTyp úlohyMax. počet bodů
(akt. za podúlohy)
Min. počet bodů
Zápočet a zkouška Zápočet a zkouška 100 (100) 51
        Zápočet Zápočet 35  15
        Zkouška Zkouška 65  20
Rozsah povinné účasti:

Zobrazit historii

Výskyt ve studijních plánech

Akademický rokProgramOborSpec.FormaJazyk výuky Konz. stř.RočníkZLTyp povinnosti
2017/2018 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2017/2018 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2016/2017 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2016/2017 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán
2015/2016 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika P čeština Ostrava 1 volitelný odborný stu. plán
2015/2016 (N2647) Informační a komunikační technologie (2612T025) Informatika a výpočetní technika K čeština Ostrava 1 volitelný odborný stu. plán

Výskyt ve speciálních blocích

Název blokuAkademický rokForma studiaJazyk výuky RočníkZLTyp blokuVlastník bloku