Formális módszerek

Ez az oldal a korábbi SCH wikiről lett áthozva.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor, kérlek, javíts rajta egy rövid szerkesztéssel!

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót.

Formális Módszerek

Tárgykód	VIMIM100
Általános infók
Szak	InfoMSC kötelező
Kredit	4
Ajánlott félév	tavasz
Keresztfélév	nincs
Tanszék	MIT
Követelmények
Jelenlét	nincs
Minimális munka	2ZH plusz házi
Labor	ősszel
KisZH	0
NagyZH	2
Házi feladat	1 + szorgalmi
Vizsga	nincs
Elérhetőségek
Levlista	form@NO-SPAM.sch.bme.hu
Tantárgyi adatlap
Tárgyhonlap

A tárgyról

• Ajánlott rövidítés: Form
• Kedvcsináló
• Levlista:
  • form@NO-SPAM.sch.bme.hu -> feliratkozás
  • infomsc@NO-SPAM.sch.bme.hu -> feliratkozás
• Régi, elavult linkek
  • Wiki: https://wiki.inf.mit.bme.hu/twiki/bin/view/Form/WebHome

Segédanyagok

Miből érdemes tanulni?

• Formális módszerek az informatikában (Typotex) - Pataricza András
• régi zh meg vizsgasorok (elég hasonló példák vannak néha)
• Előadásfóliák
• Ezen a helyen volt linkelve a(z) formcucc.pdf nevű fájl ("formcucc.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

Zh/vizsgya feladatok kidolgozva (Form Zh How to)

• Ezen a helyen volt linkelve a(z) FormJegyzet2006Osz.pdf nevű fájl ("FormJegyzet2006Osz.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

FormJegyzet2006Osz.pdf

Segédanyag az MSc-s 1. ZH-ra

• FormModVizsgaTananyag-ból az ide vonatkozó részek átemelve
  • Temporális logika - LTL, CTL és társai
  • Modellellenőrzés
  • Bináris döntési diagramok - ROBDD
  • Állapottérképek
• Bevezetés(TK 9-29)
• Ezen a helyen volt linkelve a(z) Form_LTL.pdf nevű fájl ("Form_LTL.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

Form könyvből az LTL-es rész nagyon csúnyán (de használhatóan) kiszkennelve

• LTL operátorok, és kapcsolatuk

Segédanyag az MSc-s 2. ZH-ra

• FormModVizsgaTananyag-ból az ide vonatkozó részek átemelve
  • Petri Hálók
• Definíciók
• 2. Petri Hálók (TK 31-108)
  • 2.1 Bevezetés
  • 2.2 A petri hálók struktúrája
  • 2.3 A Petri hálók dinamikus viselkedése
  • 2.4 Token Játékok
  • 2.5 Alkalmazási mintapéldák
  • 2.6 Tulajdonság modellek
  • 2.7 A Petri hálók analízis módszerei
  • 2.8 Petri háló alosztályok
  • 2.9 Analitikusan vizsgálható Petri háló alosztályok
  • 2.10 Strukurális tulajdonságok
  • 2.11 Invariánsok és alkalmazásaik
  • 2.12 Kibővített értelmezésű Petri hálók
• FormModZH2Ossz

Tapasztalatok a segédeszközökkel

• DnaNet+Ina (Windows)
• Ped+Ina-t (Linux)
• SpinEdit

UPPAAL

• Ezen a helyen volt linkelve a(z) uppaal-4.0.13.zip nevű fájl ("uppaal-4.0.13.zip" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

UPPAAL academic Java VM szükséges a futtatásához.

Régi anyagok

• Mi volt az órán?

ZH

Kidolgozott zh sorok

• Formális Módszerek ZH 2005. 04. 07. (B csoport)
• 2004 tavaszi zh megoldás
• Ezen a helyen volt linkelve a(z) form_zhmegoldasok.pdf nevű fájl ("form_zhmegoldasok.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

2006 őszi ZH megoldása

MSc-s zh sorok

• Minta ZH és minta megoldás 2011 1. ZH
  • Ezen a helyen volt linkelve a(z) FM-2011_ZH1_minta.pdf nevű fájl ("FM-2011_ZH1_minta.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

FM-2011_ZH1_minta.pdf

• • Ezen a helyen volt linkelve a(z) FM-2011_ZH1_megoldas_otletek.pdf nevű fájl ("FM-2011_ZH1_megoldas_otletek.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

FM-2011_ZH1_megoldas_otletek.pdf

• Minta ZH és receptek 2011 2. ZH
  • Ezen a helyen volt linkelve a(z) FM-2011_ZH2_PN_feladattipusok.pdf nevű fájl ("FM-2011_ZH2_PN_feladattipusok.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

FM-2011_ZH2_PN_feladattipusok

• • Ezen a helyen volt linkelve a(z) FM-2011_ZH2_PN_megoldasi_receptek.pdf nevű fájl ("FM-2011_ZH2_PN_megoldasi_receptek.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

FM-2011_ZH2_PN_megoldasi_receptek

• Ezen a helyen volt linkelve a(z) Form_masodikZH_20090607_kek.pdf nevű fájl ("Form_masodikZH_20090607_kek.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

A 2009 májusi 7.-i, 2. zh kék csoportja

• 2010 első zh
• Ezen a helyen volt linkelve a(z) form_zh1_A_100322.pdf nevű fájl ("form_zh1_A_100322.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

2010.március 22-ei Form ZH "kék" A csoportja

• Ezen a helyen volt linkelve a(z) form_zh1_B_100322.pdf nevű fájl ("form_zh1_B_100322.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

2010.március 22-ei Form ZH "fehér" B csoportja

Egyéb ZH sorok

• Ezen a helyen volt linkelve a(z) FormZH2003tavaszO.pdf nevű fájl ("FormZH2003tavaszO.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

ZH 2003 tavasz Osszes csoport

• Ezen a helyen volt linkelve a(z) FormZH2005tavaszB.pdf nevű fájl ("FormZH2005tavaszB.pdf" link szöveggel) a régi wiki http://wiki-old.sch.bme.hu/bin/view/Infoalap/FormMod oldaláról. (Ha szükséged lenne a fájlra, akkor a pontos oldalmegnevezéssel együtt küldd el a wiki@NO-SPAM.sch.bme.hu címre a kérésedet)

ZH 2005 tavasz B csoport

Vizsga

MSc-n a tárgy nem vizsgás, de érdemes csemegézni az alábbi feladatokból.
2006-os tananyaggal kapcsolatos hivatalos információk

• Formális módszerek 2002. jún. 11-i vizsga
• Formális módszerek 2004. máj. 26-i vizsga
• Formális módszerek 2004. jún. 2-i vizsga
• Formális módszerek 2006. máj. 31-i vizsga feladatok
• Formális módszerek 2006. jan. 18-i vizsga megoldása
• Formális módszerek 2007. jan. 17-ei vizsga
• FormModVizsga20070613
• FormModVizsga20080528
• FormModVizsga20080611

Házi feladat - Régi

Elérhetőek az új tanszéki weblapról: Kiírás - Segédeszközök

Bartha Tamás levele a házi feladattal kapcsolatban

Szöveges leírással megadott rendszert kell egyrészt Petri hálók segítségével modellezni és elemezni, másrészt modellellenőrzési módszerekkel verifikálni.

SAL telepítés Cygwinnel: http://sal-wiki.csl.sri.com/index.php/Cygwin_installation

Tapasztalatok az egyes feladatokkal

"A modellezés fázisában nem tiltott a feladatok szakmai konzultációja egymás közt, de kérjük, hogy alapvetően egyedül dolgozzanak."

• Házi 1-7
• Házi 8-14
• Házi 15-21
• Házi 22-28
• Házi 29-35

Mérnökinformatikus MSc
1. félév (tavasz)	Adatbiztonság  •  Formális módszerek  •  Rendszeroptimalizálás  •  Analízis  •  Tömegkiszolgálás
2. félév (ősz)	Alkalmazott algebra és matematikai logika  •  Információelmélet  •  Nyelvek és automaták  •  Szoftverarchitektúrák  •  Sztochasztika I.  •  Sztochasztika II.
Egyéb	Kötelezően választható tárgyak  •  Mérnöki menedzsment  •  Befektetések  •  Érvelés, tárgyalás, meggyőzés  •  Információs társadalom joga  •  Minőségmenedzsment  •  Projektmenedzsment  •  Vállalati jog  •  Vezetői számvitel
Szakirányok	Alkalmazott informatika  •  Autonóm irányító rendszerek és robotok  •  Hálózatok és szolgáltatások  •  Hírközlő rendszerek biztonsága  •  Intelligens rendszerek  •  Médiainformatika  •  Rendszerfejlesztés  •  Számításelmélet  •  Szolgáltatásbiztos rendszertervezés