Formális módszerek - Segédanyagok

Félév: 2012. tavasz
Cím Egyedi szöveg
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:

  1. EA09: Petri háló alapfogalmak, kiterjesztések
  2. EA10: Petri hálók dinamikus tulajdonságai
  3. EA11: Modellezés és szimuláció Petri hálókkal
  4. EA12: Elérhetőségi probléma egyszerűsítése, Petri háló alosztályok
  5. EA13: Petri hálók strukturális tulajdonságai. Dinamikus és strukturális tulajdonságok közti összefüggések.
  6. EA14: Színezett Petri hálók (1. rész)
  7. EA15: Színezett Petri hálók (2. rész)
  8. 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
Félév: 2011. tavasz
Cím Egyedi szöveg
EA01 A formális módszerek szerepe

Az előadás tartalma:

  • Tárgyadatok
  • A formális módszerek szerepe
    • Mik a formális módszerek?
    • Mire szeretnénk használni a formális módszereket?
    • A formális módszerek szerepe a fejlesztési modellekben
    • A formális módszerek értékelése
    • Sikertörténetek
  • Alapszintű formalizmusok
    • Kripke-struktúrák
    • Címkézett tranzíciós rendszerek
    • Kripke tranzíciós rendszerek
    • Időzített automaták
EA02 Temporális logikák

Az előadás tartalma:

  • Motiváció
  • Temporális logikák
  • Egy lineáris temporális logika: PLTL
    • Operátorok
    • Szintakszis
    • Szemantika
    • Példák
  • Egy elágazó idejű temporális logika: CTL*
    • Operátorok
    • Szintakszis
    • Szemantika
  • Egy másik elágazó idejű temporális logika: CTL
    • Operátorok
    • Szintakszis és szemantika
    • Példák
  • Temporális logikák kifejezőképessége
  • A modellellenőrzési feladat
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

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
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.

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
ZH1 Zárthelyi mintapéldák

Tartalom:

  • Első zárthelyi mintapéldák
  • Első zárthelyi megoldási ötletek
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ó
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
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ó
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

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
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
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
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
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.
Tartalom átvétel