Formális módszerek - Segédanyagok

Félév: 2014. 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 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: A formális modellek alkalmazásai. Állapottérképek.	Tesztgenerálás modellellenőrzővel Forráskód és monitorkód generálás Állapottérképek: szintaxis és szemantika
ZH1: Segédanyagok	Mintafeladatok Gyakorló feladatok temporális logikákhoz Gyakorló feladatok temporális logikákhoz, megoldással ZH mintapéldák (előadásfóliák)
EA06: Modellezési mintapélda	Modellezési mintapélda (előadásfóliák) Modellezési mintapélda feladatkiírás és modellek Kockadobálós játék modellek Gyalogátkelő példa modell
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 Kölcsönös kizárás Konszenzus 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ók: alapelemek és kiterjesztések Példamodellek (PetriDotNet eszközhöz)
EA08: Petri hálók dinamikus tulajdonságai. Redukció. Alosztályok.	Petri hálók dinamikus tulajdonságai Petri hálók redukciója Petri hálók alosztályai
EA09: Petri hálók strukturális tulajdonságai	Petri hálók strukturális tulajdonságai Petri hálók strukturális és dinamikus tulajdonságai közti összefüggések
EA10: Modellezés Petri hálókkal. Hierarchikus Petri hálók.	Modellezés Petri hálókkal. Hierarchikus Petri hálók.
EA11: Színezett Petri hálók	Bevezető a színezett Petri hálókhoz (egy példa) Színezett Petri hálók
ZH2: Segédanyagok	ZH2 mintafeladatok
EA12: Sztochasztikus Petri hálók	Sztochasztikus Petri hálók
EA13: Petri hálók analízise absztrakció finomítással. Adatfolyam hálók.	Petri hálók analízise ellenpélda alapú 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 Tárgyadatok
EA01: A formális módszerek szerepe	A formális módszerek szerepe Korlátok és sikertörténetek A formális módszerek szerepe
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 Alapszintű formalizmusok Lineáris temporális logikák
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) Elágazó idejű temporális logikák
E04: Modellellenőrzés	PLTL modellellenőrzés: A tabló módszer CTL modellellenőrzés: A szemantikán alapuló módszer (címkézés) Kiegészítés: PLTL modellellenőrzés automata alapú módszerrel Modellellenőrzés
EA05: Szimbolikus modellellenőrzés és ROBDD-k	Szimbolikus modellellenőrzés (bevezető) Karakterisztikus függvények ROBDD alapú reprezentáció, műveletek ROBBD-ken Szimbolikus modellellenőrzés és ROBDD-k
EA06: Korlátos modellellenőrzés	Korlátos modellenőrzés A modellellenőrzés előnyei és korlátai Tesztgenerálás modellellenőrzővel Korlátos modellellenőrzés Tesztgenerálás modellellenőrzővel
EA07: Modellezési és modellellenőrzési mintafeladat	Egy egyszerű mintapélda: kockadobálós játék Minta házi feladat: Futtatási szálak ütemezése – megoldás és ellenőrzés Minta házi feladat megoldás és ellenőrzés (fóliák) Minta házi feladat megoldás és ellenőrzés (nyomtatáshoz) Kockadobálós játék modellek Minta házi feladat: feladatkiírás és modellek Gyalogátkelő példa modell
EA08: Forráskód generálás formális modellekből	Forráskód generálás automata modellekből Monitorkód generálás futásidőbeli ellenőrzéshez Forráskód és monitorkód generálás