Formális módszerek - Segédanyagok

Félév: 2013. tavasz
Title Egyedi szöveg
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
Title 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
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
Syndicate content