Formális módszerek - Segédanyagok

Félév: 2013. tavasz
Cím Egyedi szöveg
EA01: A formális módszerek szerepe
  • A formális módszerek szerepe
  • Korlátok és sikertörténetek
EA02: Alapszintű formalizmusok. Lineáris temporális logikák.

Alapszintű formalizmusok:

  • Kripke-struktúrák (KS)
  • Címkézett tranzíciós rendszerek (LTS)
  • Kripke tranzíciós rendszerek (KTS)
  • Időzített automaták

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
  • 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)
E04: Modellellenőrzés
  • 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
  • Szimbolikus modellellenőrzés (bevezető)
  • Karakterisztikus függvények
  • ROBDD alapú reprezentáció, műveletek ROBBD-ken
EA06: Korlátos modellellenőrzés
  • 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 mintafeladat
  • Egy egyszerű mintapélda: kockadobálós játék
  • Minta házi feladat: Futtatási szálak ütemezése – megoldás és ellenőrzés
EA08: Forráskód generálás formális modellekből
  • Forráskód generálás automata modellekből
  • Monitorkód generálás futásidőbeli ellenőrzéshez
EA09: Állapottérképek
  • Állapottérképek szintaxisa
  • Állapottérképek szemantikája
  • Forráskód generálás állapottérképekből
ZH1: Segédanyagok
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
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
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
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
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
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
EA15: Színezett Petri hálók (1. rész)
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
  • 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
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
ZH2: Segédanyagok
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)
Félév: 2012. ősz
Cím Egyedi szöveg
T01: A formális módszerek szerepe
T02: Alapszintű formalizmusok
T03: Lineáris idejű temporális logikák
T04: Elágazó idejű temporális logikák
Tartalom átvétel