Formális módszerek - Segédanyagok

Félév: 2013. tavasz
Cím	Egyedi szöveg
EA09: Állapottérképek	Állapottérképek szintaxisa Állapottérképek szemantikája Forráskód generálás állapottérképekből Állapottérképek
ZH1: Segédanyagok	Mintafeladatok Gyakorló feladatok temporális logikákhoz Gyakorló feladatok temporális logikákhoz (megoldással)
GY01: Modellellenőrzési példák	A példák leírással és modellekkel együtt tölthetők le (ZIP fájlok): Kölcsönös kizárási algoritmusok ellenőrzése: Hyman, Peterson, Lamport algoritmusai Konszenzus protokoll ellenőrzése: A Paxos protokoll egy egyszerűsített verziója Feladatvégző fürt ellenőrzése: Feladatvégző egységek gyűrű struktúrában Kölcsönös kizárás Konszenzus Feladatvégző fürt
EA10: Petri háló alapfogalmak, kiterjesztések	Petri hálók felépítése, működése Dinamikus viselkedés: engedélyezettség, tüzelés, állapottrajektória Petri háló modellek készítése, alapvető modellkonstrukciók Egyszerű példák Petri hálókra Kiterjesztett Petri hálók: a tüzelési szemantika módosítása Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz) Példa modellek
EA11: Petri hálók dinamikus tulajdonságai	Elérhetőség fogalma, tulajdonságai Petri hálók dinamikus (viselkedési) tulajdonságai Állapottér reprezentációk: az elérhetőségi és fedési gráf Dinamikus tulajdonságok vizsgálata az állapottérben Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz) Példa modellek
EA12: Modellezés és szimuláció Petri hálókkal	Diszkrét rendszermodellezés alapjai Modellező eszközök: DNAnet, Snoopy, PetriDotNet Modellezési példa: Alternáló bit protokol Petri háló modellek „tesztelése”: szimuláció, token játék algoritmusai Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz) Példa modellek
EA13: Redukciós módszerek, Petri háló alosztályok	Elérhetőségi probléma egyszerűsítése Állapottér redukció Struktúra redukció Egyszerű struktúrájú Petri hálók viselkedése Petri háló alosztályok strukturális jellemzői Élő és bizt(onság)os tulajdonság kritériumai egyes alosztályokban Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz)
EA14: Petri hálók strukturális tulajdonságai	Invariánsok fogalma: T-invariáns, P-invariáns Invariánsok számítása: Martinez-Silva algoritmus Példa Petri háló modell analízisére: Alternáló bit protokoll Petri hálók további strukturális tulajdonságai Összefüggések a dinamikus és strukturális tulajdonságok között Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz) Összefüggések a dinamikus és strukturális tulajdonságok között (színes) Összefüggések a dinamikus és strukturális tulajdonságok között (szürkeárnyalatos, nyomtatáshoz) Példa modellek Példa invariáns számítás
EA15: Színezett Petri hálók (1. rész)	A színezett Petri hálók (CPN) alapjai Egyszerű protokoll CPN modellje Az "Egyszerű protokoll CPN modellje" példához további dokumentációt találhatunk angol nyelven itt Elosztott adatbázis CPN modellje Az "Elosztott adatbázis CPN modellje" példához további dokumentációt találhatunk angol nyelven itt A Design/CPN modellező eszköz tulajdonságai Dinamikus analízis lehetőségei Invariánsok Előadás fóliák (színes) Előadás fóliák (kevesebb háttérelemmel, nyomtatáshoz)
EA16: Színezett Petri hálók (2. rész)	Színezetlen és színezett Petri hálók összehasonlítása Színezett Petri hálók felépítése Színezett Petri háló példa: elosztott adatbázis Az "Elosztott adatbázis CPN modellje" példához további dokumentációt találhatunk angol nyelven itt Színezett Petri hálók működése Színezett Petri hálók széthajtogatása Színezett Petri hálók analízise Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz)
EA17: Adatfolyam hálók, modellfinomítás. Hierarchikus Petri hálók	Adatfolyam hálók: Felépítésük és formális definíciójuk. Informális szemantika: Engedélyezettség és tüzelés. Adatfolyam hálók finomítása Hierarchikus Petri hálók, modellfinomítás Finomítás Petri hálónál Hierarchikus modellezés Az "Hierarchikus protokoll CPN modellje" példához további dokumentációt találhatunk angol nyelven itt Előadás fóliák (színes) Előadás fóliák (szürkeárnyalatos, nyomtatáshoz) Példa modellek
ZH2: Segédanyagok	Mintafeladatok
EA18: Sztochasztikus Petri hálók	Alapszintű formalizmus: Folytonos idejű Markov láncok (CTMC) Modellezés: Sztochasztikus Petri hálók (SPN, GSPN, DSPN) Követelmény formalizálás: Sztochasztikus temporális logikák (CSL) Sztochasztikus Petri hálók

Félév: 2012. ősz
Cím	Egyedi szöveg
T01: A formális módszerek szerepe	A formális módszerek szerepe
T02: Alapszintű formalizmusok	Alapszintű formalizmusok
T03: Lineáris idejű temporális logikák	Lineáris idejű temporális logikák
T04: Elágazó idejű temporális logikák	Elágazó idejű temporális logikák
T05: A modellellenőrzés módszerének alapötlete	A modellellenőrzés módszerének alapötlete
T06: Állapottérképek	Állapottérképek használata
T07: Petri-hálók: alapfogalmak, kiterjesztések	Témakörök: Petri hálók felépítése, működése Petri-hálók dinamikus viselkedése Modellezés Petri hálókkal Petri háló modellek vizsgálata Kiterjesztett Petri-hálók Helyek kapacitáskorlátja Tiltó élek Prioritás Kiterjesztett és közönséges Petri-hálók kifejezőereje Petri-hálók: alapfogalmak, kiterjesztések (fóliák) Petri-hálók: alapfogalmak, kiterjesztések (nyomtatáshoz)
T08: Petri-hálók tulajdonságai	Témakörök: Petri-hálók vizsgálata Elérhetőség fogalma, tulajdonságai Petri-hálók dinamikus tulajdonságai Állapottér reprezentációk Dinamikus tulajdonságok vizsgálata az állapotérben Petri-hálók strukturális tulajdonságai Invariánsok fogalma Invariánsok számítása További strukturális tulajdonságok Strukturális és dinamikus tulajdonságok közti összefüggések Petri-hálók tulajdonságai (fóliák) Petri-hálók tulajdonságai (nyomtatáshoz)
T09: Petri-háló alapú modellek készítése	Témakörök: Közlekedési lámpa Alternáló bit protokoll A modell tulajdonságai Modellező eszközök Petri-háló alapú modellek készítése (fóliák) Petri-háló alapú modellek készítése (nyomtatáshoz)
T10: Magas szintű hálók	Témakörök: Színezett Petri-hálók felépítése CPN hálók eszközkészlete Színezett Petri-hálók működése Színezett Petri-háló példa Színezett Petri-hálók széthajtogatása Színezett Petri-hálók dinamikus tulajdonságai Színezett Petri-hálók strukturális tulajdonságai Adatfolyam háló formalizmus Adatfolyam hálók finomítása Értelmezési tartomány finomítás Struktúrafinomítás Hierarchikus Petri-hálók Hierarchikus színezett Petri-hálók Magas szintű hálók (fóliák) Magas szintű hálók (nyomtatáshoz)
T11: Modellezés színezett Petri-hálókkal	Témakörök: Modellező eszközök Példa modell: Simple protocol A modell verifikációja Másik modell: elosztott adatbázis A modell strukturális tulajdonságai Hierarchikus modellek támogatása Modellezés színezett Petri-hálókkal (fóliák) Modellezés színezett Petri-hálókkal (nyomtatáshoz)
ZH1: Segédanyagok	Ellenőrző kérdések az 1. zárthelyi dolgozathoz Mintafeladatok az 1. zárthelyi dolgozathoz Mintafeladatok az 1. zárthelyi dolgozathoz, megoldással Háttéranyag a temporális logikák témakörhöz Háttéranyag az állapottérképek témakörhöz