Formális módszerek

Formal Methods

A tantárgyleírás hatályossága

Hatályosság kezdete:

—

Hatályosság vége:

—

Tantárgy neve (magyarul, angolul)

Formális módszerek

Formal Methods

Tantárgykód

BMEVIMM3245

Tantárgyjelleg

—

Képzési szint

—

Kurzustípusok és óraszámok (heti/féléves)

Kurzustípus	elmélet	gyakorlat	laboratóriumi gyakorlat
óraszám (heti)	4	0	0
jelleg (kapcsolt/önálló)	—	—	—

Tanulmányi teljesítmény/értékelés típusa

vizsga

Tantárgy kreditértéke

Tantárgyfelelős

Dr. Pataricza András

beosztás: egyetemi docens

elérhetőség: pataricza.andras@vik.bme.hu

Tantárgyat gondozó oktatási szervezeti egység

—

Kar

Tantárgy weboldala

https://wiki.inf.mit.bme.hu/twiki/bin/view/Form/WebHome

Tantárgy elsődleges mintatantervi jellege

—

Közvetlen előkövetelmények – Erős előkövetelmény

nincs

Közvetlen előkövetelmények – Gyenge előkövetelmény

nincs

Közvetlen előkövetelmények – Párhuzamos előkövetelmény

nincs

Közvetlen előkövetelmények – Mérföldkő előkövetelmény

nincs

Közvetlen előkövetelmények – Kizáró feltétel

nincs

Célkitűzés

Tantárgyprogram

Informatikai rendszerek minőségi analízise

A formális módszerek az informatikai rendszerek tervezésében, specifikáció, modellalkotás, verifikáció, modellellenőrzés, helyességbizonyítás.

Petri hálók

Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok, tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság, perzisztencia).

Petri hálok analízis módszerei

Elérhetőségi gráf, invariánsok, Martinez-Silva algoritmus. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Predikátumok, diagnosztikai problémák modellezése. Színezett, jólformált Petri hálok (Design/CPN, WFN).

Diszkrét idejű szimuláció alapjai

Petri-háló szimulátorok felépítése, szolgáltatásai. Folyamat (workflow) modellek készítése és kiértékelése. Számítógépes kísérlettervezés alapjai.

Alkalmazások

Real-time, konkurrens és elosztott alkalmazások modellezése. Gyártásautomatizálás és ütemezés. Digitális hardware tervezés. Workflow menedzsment. Ágens technológia formális modelljei (P-gráfok).

Állapottérképek

Állapottérkép modellek felépítése, szerkezete, szintaktikája. Működés: UML és a STATEMATE szemantika. Tervezés állapottérkép alapján.

Temporális logikák

Osztályozás. Lineáris temporális logika (LTL kielégíthetőség és érvényesség). Elágazó idejű temporális logika (BTL). CTL és CTL* (érvényesség és kielégíthetőség, FairCTL). Alkalmazás konkurrens és biztonságkritikus rendszerekben. Formalizálás, komplexitás, BDD alapú reprezentáció. Műveletek ROBBD-ken.

Modellenőrzés főbb módszerei, a tableau módszer. Szimbolikus modellellenőrzés. A SAL modellellenőrző által biztosított eszközkészlet.

Processz algebrák

Konkurrens nyelvek alapjai (CSP, CCS). Speciális leíróeszközök (Ada-hálók, P-gráfok).

Adatfolyamhálók

Modellezés adatfolyam hálókkal, modellfinomítás, konzisztencia ellenőrzés finomítás után.

Alkalmazások verifikációja és validációja

Transzformáció bázisú modellverifikáció.

Az informatikai rendszerek méretének növekedésével mindinkább követelmény az, hogy a rendszer nem csak funkcionalitásában legyen helyes, hanem az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen. Ennek egyik jellegzetes trendje a formális modellekből kiinduló automatikus kódszintézis. A rendszertervezés során a kritikus elemek vizsgálatához mindinkább formális modelleken alapuló analízist alkalmaznak a rendszertervezés fázisától kezdve. A tárgy áttekintést ad az informatikai rendszerek formális minőségi és mennyiségi modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a legfontosabb matematikai leíró paradigmákat, nyelvi realizációjukat, és a kapcsolódó analitikus és szimulációs vizsgálati módszereket. Keresztmetszeti képet ad a fenti alapismeretek alkalmazásáról az informatika területén, ideértve a rendszerszintű modellezést, a hardver tervezést, a hálózati protokollok analízisét, valamint a szoftver helyességbizonyítást.

Tanulmányi eredmények

Ez a tantárgy a KKK rendeletben meghatározott, következő kompetenciák fejlesztését szolgálja:

Tudás

Nincsenek rögzített tanulási eredmények.

Képességek

Nincsenek rögzített tanulási eredmények.

Attitűd

Nincsenek rögzített tanulási eredmények.

Autonómia és felelősség

Nincsenek rögzített tanulási eredmények.

Oktatási módszertan

Előadás.

Tanulástámogató anyagok

Online források

[1] Pataricza (szerk): Formális módszerek az informatikában, 2. kiadás, Typotex, 2005.; [2] Reisig-Rozenberg: Lectures on Petri Nets Vols 1-2, Springer, 1999.; [3] Desel: Petrinetze, lineare Algebra und lineare Programmierung. Teubner 1998.; [4] Iyer-Tang: Experimental Analysis of Computer System Dependability.

A tantárgy teljesítéséhez ajánlott előzetes ismeretek

Tudás típusú kompetenciák

(azon előzetes ismeretek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)

Számítógép architektúrák, Digitális technika, Algoritmuselmélet, Számítógép hálózatok

Képesség típusú kompetenciák

(azon előzetes képességek és készségek összessége, amelyek megléte nem kötelező, de a tantárgy eredményes teljesítését nagyban elősegíti)

nincs

Ajánlott (nem kötelező) előzetesen megszerzendő kompetenciák

(azon ajánlott (nem kötelező) előzetesen megszerzendő kompetenciák összessége, amelyek jelentősen hozzájárulnak a tantárgy eredményes teljesítéséhez)

Számítógép architektúrák, Digitális technika, Algoritmuselmélet, Számítógép hálózatok

Általános szabályok

Követelmények: a. A szorgalmi időszakban: A félévvégi aláírás feltétele egy zárthelyi, továbbá egy, a tárgy anyagát felölelő konstruktív féléves házifeladat előírt színvonalú elkészítése és legalább elégséges szintű teljesítése.b. A vizsgaidőszakban:A hallgatók a tárgyból írásbeli vizsgát tesznek. A jegyhatáron lévő hallgatók számára opcionális szóbeli lehetőséget biztosítunk. Az érintett hallgatók névsorát az írásbeli eredmények kihirdetésekor tesszük közzé. A vizsgajegyben a zárthelyire és a házi feladatra kapott jegyek átlagát 10 %-os súllyal figyelembe vesszük. c. Elővizsga: nincs. Pótlási lehetőségek: A nagyzárthelyi a szorgalmi időszakban egy alkalommal, a vizsgaidőszak első 3 hetében még egy alkalommal, különeljárási díj ellenében, pótolható. A házi feladatok határidőn túl nem adhatók be, pótlásuk a vizsgaidőszakban nem lehetséges.

Teljesítményértékelési módszerek

Szorgalmi időszakban végzett teljesítményértékelések részletes leírása

Nincs megadva részletes értékelés.

Szorgalmi időszakban végzett teljesítményértékelések részaránya

Nincs megadva részarány.

Vizsgaidőszakban végzett teljesítményértékelések részletes leírása

Nincs megadva részletes értékelés.

Vizsgarészek részaránya

Nincs megadva részarány.

Érdemjegy megállapítása

Nincs megadva érdemjegy határ.

Jelenléti és részvételi követelmények

Nincs megadva jelenléti követelmény.

Javítás, ismétlés és pótlás különös szabályai

Nincs megadva.

Rövid leírás

Nincs megadva.

Részletes leírás

Nincs megadva.

Ajánlott tantárgyak

nincs.

A tantárgy elvégzéséhez szükséges tanulmányi munka

Nincs megadva munkaidő bontás.

Tantárgykövetelmények hatályossága

Tantárgykövetelmények hatályosságának kezdete:

—

Tantárgykövetelmények hatályosságának vége:

—

Tantervi elhelyezés

Nincsenek rögzített tantervi elhelyezések ehhez a tárgyverzióhoz.