A tantárgyleírás hatályossága
Hatályosság kezdete:
2026. March 21.
Hatályosság vége:
—
| Tantárgy neve (magyarul, angolul) |
Formális módszerek
Formal Methods
|
||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Tantárgykód | BMEVIMIM100 | ||||||||||||
| Tantárgyjelleg | — | ||||||||||||
| Képzési szint | — | ||||||||||||
| Kurzustípusok és óraszámok (heti/féléves) |
|
||||||||||||
| Tanulmányi teljesítmény/értékelés típusa | félévközi érdemjegy | ||||||||||||
| Tantárgy kreditértéke | 4 | ||||||||||||
| Tantárgyfelelős |
DR. Majzik István
beosztás: egyetemi docens
elérhetőség:
majzik.istvan@vik.bme.hu
|
||||||||||||
| Tantárgyat gondozó oktatási szervezeti egység |
Mesterséges Intelligencia és Rendszertervezés Tanszék
|
||||||||||||
| Kar | Villamosmérnöki és Informatikai Kar | ||||||||||||
| Tantárgy weboldala | http://www.mit.bme.hu/oktatas/targyak/vimim100/ | ||||||||||||
| 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 formális modellezése és analízise (a tantárgy összefoglaló bevezetése): A formális módszerek szerepe az informatikai rendszerek tervezésében: követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás). Mérnöki és formális modellek kapcsolata, modell-transzformációk.
- Alapszintű formális modellek és szemantikák: Kripke-struktúrák, tranzíciós rendszerek, időzített automaták, automaták hálózata.
- Követelmények formalizálása temporális logikákkal: Lineáris temporális logika (LTL). Elágazó idejű temporális logikák (CTL, CTL*). Gyakorlati példák és alkalmazások (PSL).
- Formális verifikáció modellellenőrzéssel: Modellellenőrzés tabló módszerrel, valamint szimbolikus technikákkal. Bináris döntési diagramok használata. Korlátos modell ellenőrzés. Gyakorlati alkalmazások: Egyszerű algoritmusok helyességének verifikálása (UPPAAL), tesztgenerálás modell ellenőrzővel.
- Informatikai rendszerek dinamikus viselkedésének modellezése állapottérképekkel: Állapottérképek szintaktikája és szemantikája. Tervezés állapottérképek alapján. Gyakorlati alkalmazások: UML állapottérképek, szoftver forráskód generálás, biztonságkritikus rendszerek tervezése (SCADE).
- Modellezés Petri hálókkal: Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok. Tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság). Elérhetőségi gráf, invariánsok. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Színezett Petri hálók. Gyakorlati alkalmazások: Adatbázis kezelő konzisztencia vizsgálata, protokoll analízis.
- Modellezés adatfolyam hálókkal: Adatfolyam hálók szintaktikája és szemantikája. Modellfinomítás, a finomítás konzisztenciájának ellenőrzése. Adatfolyam hálók alkalmazása üzleti folyamatok modellezésére és szolgáltatásbiztonságának ellenőrzésére. Gyakorlati alkalmazások: IBM Business Modeller, SCADE.
- Informatikai rendszerek mérnöki modellezése és analízise: Metamodellezés, modelltranszformációk. Mintapéldák UML modellek formális verifikációjára.
Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével mindinkább követelmény az, hogy a kritikus komponensek megvalósítása bizonyítottan helyes legyen. Ennek egyik jellegzetes megoldása a formális modelleken alapuló tervezés és megvalósítás: A formális modellek analízisével vizsgálhatóvá válnak a tervezői döntések, bizonyíthatóak egyes tulajdonságok, valamint automatizálható a kódszintézis. A tárgy áttekintést ad az informatikai rendszerek formális 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, a modellezési nyelveket, valamint a kapcsolódó analitikus és szimulációs vizsgálati módszereket. Demonstrálja ezek alkalmazását a rendszerszintű modellezés, a hardver tervezés, valamint a szoftver helyességbizonyítás és szintézis területén.
A tantárgy követelményeit eredményesen teljesítő hallgatók
megismerik és alkalmazni tudják a különböző formális módszereket és technológiákat,
képesek lesznek nem-formális rendszer leírások alapján matematikai modellt alkotni,
megismerik a különböző helyességbizonyítási technikák előnyeit és hátrányait,
tisztában lesznek a formális módszereket támogató alapvető eszközökkel.
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
Pataricza András (szerk.): Formális módszerek az informatikában. TypoTeX Kiadó, 2005.; Ajánlott irodalom:; W. Reisig, G. Rozenberg (eds.): Lectures on Petri Nets. Vol I-II, Springer Verlag, 1998.; D. Peled: Software Reliability Methods. Springer Verlag, 2001.; E. M. Clarke, O. Grumberg, D. Peled: Model Checking. MIT Press, 2000.; G. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991.
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)
-
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)
-
Általános szabályok
Követelmények:
A szorgalmi időszakban: A félévközi jegy megszerzésének követelménye két zárthelyi és egy házi feladat legalább elégséges szintű teljesítése. A házi feladat részei egy kisméretű információs rendszer modelljének elkészítése valamint az elvárt tulajdonságok modell alapú analízise. A házi feladat kiadására a 4. oktatási héten kerül sor, a beadásához kapcsolódó beszámolók, ill. bemutatók a 10. oktatási héttől ütemezhetők. A félévközi jegyet 35-35%-os súllyal a két zárthelyi osztályzata és 30%-os súllyal a házi feladat osztályzata határozza meg.
A vizsgaidőszakban: -
Pótlási lehetőségek:
A szorgalmi időszakban bármelyik zárthelyi pótlására van lehetőség, de egy hallgató csak egy zárthelyit pótolhat. Egy sikertelen zárthelyi újbóli pótlására a pótlási időszakban is van lehetőség. Házi feladatok határidőn túl a pótlási héten adhatók be, a késedelmes beadás 20% pontlevonással jár.
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
-
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.