Formális módszerek - Segédanyagok

Félév: 2015. tavasz
Cím Egyedi szöveg
EA12: Sztochasztikus Petri hálók
ZH2: Gyakorló feladatok
EA13: Absztrakció a modellellenőrzésben
EA14: Adatfolyam hálók
Félév: 2014. tavasz
Cím Egyedi szöveg
EA00: Tárgyadatok
EA01: A formális módszerek szerepe. Alapszintű formalizmusok.
EA02: Követelmények formalizálása temporális logikákkal
EA03: Modellellenőrzés
EA04: Hatékony technikák modellellenőrzéshez
EA05: A formális modellek alkalmazásai. Állapottérképek.
ZH1: Segédanyagok
EA06: Modellezési mintapélda
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
EA07: Petri hálók: alapelemek és kiterjesztések

A példamodellekhez használható PetriDotNet eszköz letölthető a szorgalmi feladat oldalról.

EA08: Petri hálók dinamikus tulajdonságai. Redukció. Alosztályok.
EA09: Petri hálók strukturális tulajdonságai
EA10: Modellezés Petri hálókkal. Hierarchikus Petri hálók.
EA11: Színezett Petri hálók
ZH2: Segédanyagok
EA12: Sztochasztikus Petri hálók
EA13: Petri hálók analízise absztrakció finomítással. Adatfolyam hálók.
Félév: 2013. tavasz
Cím Egyedi szöveg
EA00: Tárgyadatok

Tárgyadatok, követelmények

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