Formális módszerek - Segédanyagok

Félév: 2017. tavasz
Cím	Egyedi szöveg
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
EA03: Modellellenőrzés	Modellellenőrzés Esettanulmány: A PSL tulajdonságleíró nyelv és használata Esettanulmány: PLC prrogramok modellellenőrzése
EA04: Hatékony technikák modellellenőrzéshez	Szimbolikus modellellenőrzés és ROBDD-k Korlátos modellellenőrzés
EA05 Állapottérképek. Tesztgenerálás modellellenőrzővel.	Állapottérképek: szintaxis és szemantika Tesztgenerálás modellellenőrzővel
ZH1 segédanyagok	ZH1 mintapéldák (diasor) ZH1 mintafeladatsor ZH1 további feladatsor (1) ZH1 további feladatsor (2) Gyakorló feladatok temporális logikákhoz Gyakorló feladatok temporális logikákhoz, megoldással
EA06: Szoftverek modellellenőrzése. HF mintapéldák.	Szoftver modellellenőrzés Modellezési példa: Kockajáték (bemutató) Modellezési példa: Kockajáték (modellek) Modellezési példa: Bit protokoll (bemutató) Modellezési példa: Bit protokoll (modell) UPPAAL összefoglaló
HF1: Modellellenőrzési példák	A példák leírással és modellekkel együtt tölthetők le (ZIP fájlok). 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
EA07: Petri hálók: alapelemek és kiterjesztések	A példamodellekhez használható PetriDotNet eszköz letölthető a szorgalmi feladat oldalról. Petri háló alapelemek és kiterjesztések Példamodellek (PetriDotNet eszközhöz)
EA08: Petri hálók dinamikus tulajdonságai. Redukciók.	Modellezés Petri hálókkal Petri hálók dinamikus tulajdonságai Redukciók az állapottérben és a Petri háló struktúrájában
EA09: Petri hálók strukturális tulajdonságai. Petri hálók analízise.	Petri hálók strukturális tulajdonságai. Invariánsok számítása. Petri hálók analízise Példamodell: Az Alternating Bit Protocol
EA10: Hierarchikus Petri hálók. Színezett Petri hálók.	Hierarchikus Petri hálók Színezett Petri hálók
EA11: Modellezés színezett Petri-hálókkal. Gyakorló feladatok	Modellezés színezett Petri-hálókkal Gyakorló feladatok
EA12: Sztochasztikus Petri hálók	Sztochasztikus Petri hálók. Sztochasztikus temporális logikák.
ZH2 segédanyagok	ZH2 minta feladatsor (1) ZH2 minta feladatsor (2)

Félév: 2016. tavasz
Cím	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
EA03: Modellellenőrzés	Modellellenőrzés A PSL tulajdonságleíró nyelv és használata
EA04: Hatékony technikák modellellenőrzéshez	Szimbolikus modellellenőrzés és ROBDD-k Korlátos modellellenőrzés
EA05: Ekvivalencia ellenőrzés. A formális modellek alkalmazásai.	Modellek ekvivalenciájának és finomításának ellenőrzése Tesztgenerálás modellellenőrzővel Forráskód és monitorkód generálás
EA06: Állapottérképek. Modellezési mintapéldák.	A modellezési példák leírással és modellekkel együtt tölthetők le (ZIP fájlok). Állapottérképek: szintaxis és szemantika Modellezési mintapélda: Kockajáték Modellezési mintapélda: Alternáló bit protokoll
ZH1: Gyakorló feladatok	ZH1 mintapéldák (diasor) ZH1 mintafeladatsor ZH1 további példák (1) ZH1 további példák (2) Gyakorló feladatok temporális logikákhoz Gyakorló feladatok temporális logikákhoz, megoldással
HF1: Modellellenőrzési példák	A példák leírással és modellekkel együtt tölthetők le (ZIP fájlok). 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
EA07: Petri hálók: alapelemek és kiterjesztések	A példamodellekhez használható PetriDotNet eszköz letölthető a szorgalmi feladat oldalról. Petri háló alapelemek és kiterjesztések Példamodellek (PetriDotNet eszközhöz)