Formális módszerek - Segédanyagok

Félév: 2019. tavasz
Title	Egyedi szöveg
EA07: Modellezési mintapéldák	Modellezési példa: Kockajáték (diasor) Modellezési példa: Kockajáték (modellek, ZIP) Modellezési példa: Alternáló bit protokoll (diasor) Modellezési példa: Alternáló bit protokoll (modell, ZIP) Tesztgenerálás modellellenőrzővel (diasor) Modellezési mintapélda: Meltdown sérülékenység (diasor) Modellezési mintapélda: Meltdown sérülékenység (modell, ZIP) UPPAAL modellezési lehetőségek összefoglalása (diasor)
HF: Modellellenőrzési példák	A példák leírással és modellekkel együtt tölthetők le. Futási szálak kezelése Kölcsönös kizárás algoritmusok Konszenzus egyszerűsített Paxos protokollal Feladatvégző fürt
EA08: Petri hálók: alapelemek és kiterjesztések	PetriDotNet eszköz és dokumentáció: ld. a szorgalmi feladat web lapján. Petri háló alapelemek és kiterjesztések A bemutatott PetriDotNet modellek (ZIP-ben)
EA09: Petri hálók dinamikus tulajdonságai. Redukciók.	Modellezés Petri hálókkal Petri hálók dinamikus tulajdonságai Redukciók a Petri háló struktúrájában
EA10: Petri hálók strukturális tulajdonságai. Hierarchikus Petri hálók.	Petri hálók strukturális tulajdonságai. Invariánsok és számításuk. Petri hálók analízise: mintapélda Hierarchikus Petri hálók Példamodell: Az Alternating Bit Protocol (ZIP, PetriDotNet eszközhöz)
EA11: Színezett Petri hálók	Színezett Petri hálók. Modellezés és analízis színezett Petri-hálókkal.
EA12: Sztochasztikus Petri hálók	Sztochasztikus Petri hálók
ZH2: Segédanyagok	ZH2 gyakorló feladatok (diasor) ZH2 gyakorló feladatsor ZH2 gyakorló feladatsor megoldással (angolul) (1) ZH2 gyakorló feladatsor megoldással (angolul) (2)

Félév: 2018. tavasz
Title	Egyedi szöveg
EA00: Tárgyadatok	Tárgyadatok
EA01: A formális módszerek szerepe. Alapszintű formalizmusok.	A formális módszerek szerepe Alapszintű formalizmusok
EA02: Követelmények formalizálása temporális logikákkal	Lineáris idejű temporális logikák Elágazó idejű temporális logikák Mintapélda: A Property Specification Language (PSL) nyelv
EA03: Modellellenőrzés	Modellellenőrzés Modellellenőrzők: A SPIN eszköz és a Promela nyelv
EA04: Hatékony technikák modellellenőrzéshez	Szimbolikus modellellenőrzés és ROBDD-k Korlátos modellellenőrzés Modellellenőrzők: A NuSMV eszköz Esettanulmány: PLC programok modellellenőrzése a CERN-ben
EA05 Állapottérképek	Állapottérképek: szintaxis és szemantika
ZH1: Segédanyagok	ZH1 gyakorló feladatok (diasor) ZH1 mintafeladatsor (1) ZH1 mintafeladatsor (2) ZH1 mintafeladatsor (3) Gyakorló feladatok (szöveges) Gyakorló feladatok (szöveges, megoldással) ZH1 mintafeladatsor megoldással (angolul) (1) ZH1 mintafeladatsor megoldással (angolul) (2)
EA06: Szoftverek modellellenőrzése. Modellezési mintapélda.	Szoftver-modellellenőrzés absztrakciós módszerekkel Modellezési mintapélda: Meltdown sérülékenység (diasor) Modellezési mintapélda: Meltdown sérülékenység (modell, ZIP)
EA07: Modellezési mintapéldák	Szoftver-modellellenőrző: A CPAchecker eszköz Tesztgenerálás modellellenőrzővel Modellezési példa: Kockajáték (diasor) Modellezési példa: Kockajáték (modellek, ZIP) Modellezési példa: Alternáló bit protokoll (diasor) Modellezési példa: Alternáló bit protokoll (modell, ZIP) UPPAAL modellezési lehetőségek (összefoglaló, diasor)
HF: Modellellenőrzési példák	A példák leírással és modellekkel együtt tölthetők le. Futási szálak kezelése Kölcsönös kizárás (Hyman, Peterson, Lamport algoritmusok) Konszenzus (egyszerűsített Paxos protokoll) Feladatvégző fürt
EA08: Petri hálók: alapelemek és kiterjesztések	PetriDotNet eszköz és dokumentáció: ld. a szorgalmi feladat w eb lapján. Petri háló alapelemek és kiterjesztések Példamodellek (PetriDotNet eszközhöz)
EA09: Petri hálók dinamikus tulajdonságai. Redukciók.	Modellezés Petri hálókkal Petri hálók dinamikus tulajdonságai Redukciók a Petri háló struktúrájában
EA10: Petri hálók strukturális tulajdonságai. Hierarchikus Petri hálók.	Petri hálók strukturális tulajdonságai. Invariánsok és számításuk. Petri hálók analízise: mintapélda Hierarchikus Petri hálók Példamodell: Az Alternating Bit Protocol
EA11: Színezett Petri hálók	Színezett Petri hálók. Modellezés és analízis színezett Petri-hálókkal.
EA12: Sztochasztikus Petri hálók	Sztochasztikus Petri hálók
ZH2: Segédanyagok	ZH2 gyakorló feladatok (diasor) ZH2 mintafeladatsor ZH2 mintafeladatsor megoldással (angolul) (1) ZH2 mintafeladatsor megoldással (angolul) (2)

Félév: 2017. tavasz
Title	Egyedi szöveg
EA00: Tárgyadatok	Tárgyadatok