|
EA01: A formális módszerek szerepe |
Az előadás tartalma:
-
Tárgyadatok
-
A formális módszerek szerepe
-
Mintapélda: Egy fejlesztői keretrendszer bemutatása
|
|
EA02: Alapszintű formalizmusok és lineáris idejű temporális logikák |
Az előadás anyaga:
Alapszintű formalizmusok:
-
Kripke-struktúrák (KS)
-
Címkézett tranzíciós rendszerek (LTS)
-
Kripke tranzíciós rendszerek (KTS)
-
Véges állapotú automaták időkezeléssel
Lineáris idejű temporális logikák:
-
Temporális logikák típusai
-
Lineáris idejű temporális logikák
-
PLTL: Operátorok, formális szintaxis és szemantika
-
Követelmények formalizálása
|
|
EA03: Elágazó idejű temporális logikák |
Az előadás anyaga:
-
CTL*: Operátorok, mintapéldák, formális szintaxis és szemantika
-
CTL: Kötöttségek, szintaxis és szemantika
-
Követelmények formalizálása (példák)
|
|
EA04: Modellellenőrzés |
Az előadás anyaga:
-
PLTL modellellenőrzés: A tabló módszer
-
CTL modellellenőrzés: A szemantikán alapuló módszer (címkézés)
-
Kiegészítés: PLTL modellellenőrzés automata alapú módszerrel
|
|
EA05: Szimbolikus modellellenőrzés és ROBDD-k |
Az előadás anyaga:
-
Szimbolikus modellellenőrzés (bevezető)
-
Karakterisztikus függvények
-
ROBDD alapú reprezentáció, műveletek ROBBD-ken
|
|
EA06: Korlátos modellellenőrzés |
Az előadás anyaga:
-
Korlátos modellenőrzés
-
A modellellenőrzés előnyei és korlátai
-
Tesztgenerálás modellellenőrzővel
|
|
EA07: Modellezési és modellellenőrzési mintapélda (házi feladathoz) |
Az előadás anyaga:
-
Egy modellellenőrzési mintapélda kidolgozása UPPAAL környezetben
|
|
MM01: 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
|
|
EA08: Állapottérképek és forráskód generálás |
Az előadás anyaga:
-
Alkalmazás forráskód generálás automaták alapján
-
Monitor forráskód generálás formális modell és követelmények alapján
-
UML állapottérképek szintaxisa és szemantikája
-
Kódgenerálás állapottérképek alapján
|
|
ZH1: Mintafeladatok az első zárthelyihez |
A letölthető anyagok:
-
Mintafeladatok az első zárthelyihez
-
Megoldási ötletek. Hibajavítás: A 2.3 feladat harmadik diagramján az (1,y22) csomópontból a szaggatott élet az (1,z2) csomóponthoz kell húzni a (z1,1) csomópont helyett!
|
|
EA09: 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
-
Engedélyezettség feltétele
-
Állapotátmenet
-
Szomszédossági mátrix
-
Tüzelési szekvencia
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
-
Korlátos kapacitású hely
-
Kiegészítő helytranszformáció
-
Tiltó él
-
Prioritás
|
|
EA10: Petri hálók dinamikus tulajdonságai |
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 állapottérben
|
|
EA11: Modellezés és szimuláció Petri hálókkal |
Az előadás tartalma:
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
-
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
|
|
EA12: Elérhetőségi probléma egyszerűsítése, Petri háló alosztályok |
Az előadás tartalma:
Elérhetőségi probléma egyszerűsítése
-
Állapottér redukció
-
A részleges sorrendezési reláción alapuló redukció alapötlete
-
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
|
|
EA13: Petri hálók strukturális tulajdonságai |
Az előadás tartalma:
Invariánsok fogalma
-
Állapotegyenlet
-
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
-
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
|
|
EA14: Színezett Petri hálók (1. rész) |
Az előadás tartalma:
-
A színezett Petri hálók (CPN) alapjai
-
Egyszerű protokoll CPN modellje
-
Elosztott adatbáziskezelő rendszer modellje
-
A Design/CPN modellező eszköz tulajdonságai
-
Dinamikus analízis lehetőségei
-
Dinamikus tulajdonságok
-
Állapottér lekérdezések
-
ASKCTL temporális logikai kérdések
-
Invariánsok
|
|
EA15: Színezett Petri hálók (2. rész) |
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ó 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
-
Színezett Petri hálók széthajtogatása
-
Színezett Petri hálók analízise
-
Dinamikus tulajdonságok
-
Invariánsok
|
|
EA16: Adatfolyam hálók, modellfinomítás. Hierarchikus Petri 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
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, a Snoopy és a DNAnet eszközökben
-
Hierarchikus színezett Petri hálók
|
|
ZH2: Petri hálós előadások fóliái nyomtatáshoz |
A mellékelt PDF fájlok az alábbi előadások anyagát tartalmazzák nyomtatásra alkalmas (fehér háttér, fekete betűk, szürkeárnyalatos ábrák) formában:
-
EA09: Petri háló alapfogalmak, kiterjesztések
-
EA10: Petri hálók dinamikus tulajdonságai
-
EA11: Modellezés és szimuláció Petri hálókkal
-
EA12: Elérhetőségi probléma egyszerűsítése, Petri háló alosztályok
-
EA13: Petri hálók strukturális tulajdonságai. Dinamikus és strukturális tulajdonságok közti összefüggések.
-
EA14: Színezett Petri hálók (1. rész)
-
EA15: Színezett Petri hálók (2. rész)
-
EA16: Adatfolyam hálók, modellfinomítás. Hierarchikus Petri hálók
|
|
EA17: Sztochasztikus Petri hálók |
Az előadás anyaga:
-
Alapszintű formalizmus: Folytonos idejű Markov láncok
-
Sztochasztikus Petri hálók (SPN, GSPN, DSPN)
-
Sztochasztikus temporális logikák (CSL)
|
|
ZH2: Mintafeladatok a második zárthelyihez |
A letölthető anyag:
-
Mintafeladatok a második zárthelyihez
|
