Formális módszerek - Segédanyagok

Félév: 2020. 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 A bemutatott UPPAAL modellek (ZIP-ben)
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 A modellellenőrzési feladat (bevezető) A bemutatott UPPAAL modellek (ZIP-ben) Kiegészítő példa: A Property Specification Language (PSL)
EA03: Modellellenőrzés	Modellellenőrzés Modellellenőrzők: A SPIN eszköz és a Promela nyelv A bemutatott Promela modellek (ZIP-ben)
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 A bemutatott NuSMV modellek (ZIP-ben) Kiegészítő példa: PLC programok modellellenőrzése a CERN-ben
EA05 Állapottérképek	Állapottérképek szintaxisa és szemantikája
ZH1 Segédanyagok	ZH1 gyakorló feladatok (diasor) ZH1 mintafeladatsor (1) ZH1 mintafeladatsor (2) ZH1 mintafeladatsor (3) Néhány gyakorló feladat (szöveges, megoldással) ZH1 mintafeladatsor megoldással (angolul) (1) ZH1 mintafeladatsor megoldással (angolul) (2) ZH1 mintafeladatsor megoldással (angolul) (3) ZH1 mintafeladatsor megoldással (angolul) (4)
EA06: Szoftverek modellellenőrzése	Szoftver-modellellenőrzés absztrakciós módszerekkel Mintapélda: Solc-Verify: A Modular Verifier for Solidity Smart Contracts
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	Modellezés Petri-hálókkal Petri-hálók dinamikus tulajdonságai Tulajdonságmegőrző redukciók
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
EA13: Gyakorló feladatok	ZH2 gyakorló feladatok
ZH2 Segédanyagok	ZH2 gyakorló feladatsor ZH2 gyakorló feladatsor megoldással (angolul) (1) ZH2 gyakorló feladatsor megoldással (angolul) (2)

Félév: 2019. 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 A bemutatott UPPAAL modellek (ZIP-ben)
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 A modellellenőrzési feladat (bevezető) A bemutatott UPPAAL modellek (ZIP-ben) Kiegészítő példa: A Property Specification Language (PSL)
EA03: Modellellenőrzés	Modellellenőrzés Modellellenőrzők: A SPIN eszköz és a Promela nyelv A bemutatott Promela modellek (ZIP-ben)
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 A bemutatott NuSMV modellek (ZIP-ben) Kiegészítő példa: PLC programok modellellenőrzése a CERN-ben
EA05 Állapottérképek	Állapottérképek szintaxisa és szemantikája
ZH1: Segédanyagok	ZH1 gyakorló feladatok (diasor) ZH1 mintafeladatsor (1) ZH1 mintafeladatsor (2) ZH1 mintafeladatsor (3) Gyakorló feladatok (szöveges, megoldással) ZH1 mintafeladatsor megoldással (angolul) (1) ZH1 mintafeladatsor megoldással (angolul) (2) ZH1 mintafeladatsor megoldással (angolul) (3) ZH1 mintafeladatsor megoldással (angolul) (4)
EA06: Szoftverek modellellenőrzése	Szoftverek modellellenőrzése Szoftver-modellellenőrző: A CPAchecker eszköz