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 | BMEVIMIMA19 | ||||||||||||
| 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 | 3 | ||||||||||||
| 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 | — | ||||||||||||
| 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 szimbolikus technikákkal. 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, Yakindu Statechart Tools.
- Modellezés Petri hálókkal: Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok. Dinamikus tulajdonságok (elérhetőség, korlátosság, megfordíthatóság, visszatérő állapotok, élő tulajdonság). Elérhetőségi gráf. Strukturális tulajdonságok (invariánsok). Redukciós technikák. Gyakorlati alkalmazások: protokoll analízis.
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. 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, valamint a szoftver helyességbizonyítás területén.
A tantárgy követelményeit
eredményesen teljesítő hallgatók
megismerik és alkalmazni tudnak egyes 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
Ajánlott irodalom:; Pataricza András (szerk.): Formális módszerek az; informatikában. TypoTeX Kiadó, 2005.; 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)
nincs
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)
nincs
Általános szabályok
Követelmények:
A szorgalmi időszakban:
A félévközi jegy megszerzésének követelménye egy zárthelyi dolgozat é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 70%-os súllyal a 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 zárthelyi dolgozat egy alkalommal
a szorgalmi időszakban pótolható vagy javítható. Sikertelen zárthelyi pótlására
egy alkalommal a pótlási időszakban is van lehetőség. Házi feladatok határidőn
túl a pótlási időszakban 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
Nincs megadva.
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.