Formális módszerek - Segédanyagok

Félév: 2012. ősz
Cím Egyedi szöveg
T05: A modellellenőrzés módszerének alapötlete
T06: Állapottérképek
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
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
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
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
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
ZH1: Segédanyagok
HF: Házi feladat
ZH2: Mintafeladatok
Félév: 2012. 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
  • 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

Tartalom átvétel