Formális módszerek - Segédanyagok

Félév: 2011. tavasz
Title	Egyedi szöveg
EA03 Modellellenőrzés	Az előadás tartalma PLTL modellellenőrzés A tabló módszer Kiegészítő anyag: Automata alapú modellellenőrzés CTL modellellenőrzés A szemantika alapú módszer: Állapotok címkézése Tesztgenerálás modellellenőrzővel Modellellenőrzés Példa: Tesztgenerálás modellellenőrzővel
EA04 Hatékony modellellenőrzés	Az előadás tartalma: Szimbolikus modellellenőrzés Állapothalmazok kezelése Karakterisztikus függvények Karakterisztikus függvények kezelése ROBDD-vel Az ROBDD-k tulajdonságai ROBDD építése Műveletek ROBDD-ken Korlátos modellellenőrzés A SAT megoldók használata A modellellenőrzés algoritmusa Szoftver modellellenőrzés Hatékony modellellenőrzés
MM01: Modellellenőrzési példák	Tartalom: Kölcsönös kizárási algoritmusok ellenőrzése Hyman algoritmusa Peterson algoritmusa Lamport algoritmusa 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 A mintapéldák leírással és modellekkel együtt ZIP fájlokban tölthetők le. Kölcsönös kizárási algoritmusok Konszenzus protokoll Feladatvégző fürt
EA05 Állapottérképek	Az előadás tartalma: Állapottérképek Modell elemek Informális szemantika Formális szemantika (kiegészítő anyag) Forráskód generálás Forráskód generálás időzített automaták alapján (áttekintés) Kódgenerálási minták állapottérképekhez Monitorkód generálás állapottérkép referencia alapján Állapottérképek
ZH1 Zárthelyi mintapéldák	Tartalom: Első zárthelyi mintapéldák Első zárthelyi megoldási ötletek Első zárthelyi mintapéldák Első zárthelyi megoldási ötletek Automaták összevonása, több automatából álló rendszer együttes állapottere
EA06 Petri háló alapfogalmak, kiterjesztések	Az előadás tartalma: Petri hálók felépítése, működése Petri hálók alapvető tulajdonságai Petri hálók struktúrája Petri hálók állapota, működ(tet)ése, dinamika Dinamikus viselkedés: engedélyezettség, tüzelés, állapottrajektória Engedélyezettség feltétele Állapotátmenet Szomszédossági mátrix Tüzelési szekvencia Petri háló modellek készítése, aAlapvető konstrukciók Modellező eszközök: DNAnet, Snoopy, PetriDotNet Egyszerű példák Petri hálókra Kiterjesztett Petri hálók: a tüzelési szemantika módosítása Tiltó él Prioritás Korlátos kapacitású hely Kiegészítő helytranszformáció Előadás fóliák Példa Petri háló modellek
EA07 Modellezés és szimuláció Petri hálókkal	Az előadás tartalma: Diszkrét rendszermodellezés alapjai Folyamatorientált modellezés Tevékenységek modellezése Petri hálókban Erőforrás allokáció Petri hálókban Rendszermodellezés Automaták összevonása, direkt szorzat A rendszer finomítása: feltételek, szinkronizáció Egyszerű példa automatákkal és Petri hálóval Egy összetettebb szöveges példa Hierarchikus Petri hálók, modellfinomítás Hierarchikus modellfinomítás Kompozícionalitás (Petri hálók) Finomítás, erőforrás modellezés Hierarchikus felépítés eszközei Petri háló modellek „tesztelése”: szimuláció, token játék algoritmusai Petri hálók szimulációja Egyszerű szimulációs algoritmus Hatékony szimulációs algoritmus Prioritásos Petri hálók szimulációja Időzítés kezelése Előadás fóliák Diszkrét rendszermodellezés: annotált fóliák Példa Petri háló modellek
EA08 Petri hálók dinamikus tulajdonságai	A 15. fólián levő "hibát" (ez az előadáson bemutatott animáció utolsó állapota) javítottam. Tisztelettel kérem a hallgatóságot, hogy ha ilyen jellegű hibát, elírást talál, legyenek szívesek nekem (is) jelezni! Az előadás tartalma: Elérhetőség fogalma, tulajdonságai Elérhetőség, elérhetőségi probléma Petri hálók dinamikus (viselkedési) tulajdonságai Korlátosság Élőség Megfordíthatóság Visszatérő állapot Fedhetőség Perzisztencia Korlátozott fairség (B-fairség) Globális fairség Állapottér reprezentációk: az elérhetőségi és fedési gráf Elérhetőségi gráf Fedési gráf Fedési fa generáló algoritmus Petri hálók fedési fájának analízise Dinamikus tulajdonságok vizsgálata az állapotérben Petri hálók redukciós módszerei Állapottér redukció Struktúra redukció Előadás fóliák Példa Petri háló modellek
EA09 Petri hálók strukturális tulajdonságai	Az előadás tartalma: Elérhetőségi probléma egyszerűsítése Struktúra redukció Soros összevonások Párhuzamos összevonások Egyszerű struktúrájú Petri hálók viselkedése Petri háló alosztályok Állapotgép (State Machine, SM) Jelölt gráf (Marked Graph, MG) Szabad választású háló (Free-Choice Net, FC) Kiterjesztett szabad választású háló (EFC) Aszimmetrikus választású háló (AC) Élő és bizt(onság)os tulajdonság kritériumai Invariánsok fogalma Tüzelési, avagy T-invariáns Hely, avagy P-invariáns Invariánsok számítása Martinez-Silva algoritmus Petri hálók további strukturális tulajdonságai Állapotegyenlet Strukturális korlátosság Vezérelhetőség Konzervativitás Strukturális élőség Ismételhetőség Konzisztencia Példa Petri háló modell analízisére: Alternáló bit protokoll Előadás fóliák Példa Petri háló modellek Példa invariáns számításra + DNAnet modell
EA10 Színezett Petri hálók 1.	Az előadás tartalma: A színezett Petri hálók (CPN) alapjai Egy egyszerű protokoll CPN modellje A Design/CPN modellező eszköz tulajdonságai Dinamikus analízis lehetőségei Előadás fóliák Az egyszerű protokoll CPN modelljének leírása (angol)
EA11 Színezett Petri hálók 2.	Az előadás tartalma: 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ó alkotóelemei Multihalmazok Coloured Petri Nets (CPN) hálók eszközkészlete Színezett Petri háló példa: elosztott adatbázis Színezett Petri hálók működése Engedélyezettség színezett Petri hálókban Őrfeltétel Tüzelés színezett Petri hálókban Lekötött és lekötetlen változók Hierarchikus Petri hálók, modellfinomítás Finomítás Petri hálónál Hierarchikus modellezés Hierarchikus felépítés eszközei a PetriDotNet, Snoopy éa DNAnet eszközökben Hierarchikus színezett Petri hálók Színezett Petri hálók széthajtogatása Előadás fóliák Elosztott adabázis CPN modelljének leírása (angol) Egyszerű protokoll hierarchikus CPN modelljének leírása (angol) Példa Petri háló modellek
EA13 Sztochasztikus Petri hálók	Az előadás tartalma: Motiváció Sztochasztikus folyamatok és modellek Folytonos idejű Markov láncok Sztochasztikus Petri-hálók SPN, GSPN, DSPN, TPN, SRN Időzítési szemantikák Követelmények formalizálása Sztochasztikus temporális logikák Sztochasztikus Petri hálók (előadásfóliák)
ZH2 Zárthelyi mintapéldák	Tartalom: Második zárthelyi tipikus feladatok (nem csak ezek lehetségesek!) Második zárthelyi megoldási receptek ZH2 Petri háló feladattípusok ZH2 megoldási receptek
EA14 Adatfolyam hálók	Az előadás tartalma: 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: A finomítás módszerei, értelmezési tartomány (állapot- és tokenfinomítés) és struktúra finomítása. Konzisztencia ellenőrzés finomítás után. Adatfolyam hálók és finomításuk Adatfolyam hálók széthajtogatása