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 | BMEVIMIMA26 | ||||||||||||
| 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 | 5 | ||||||||||||
| 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/VIMIMA26 | ||||||||||||
| 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
- A formális módszerek szerepe az informatikai rendszerek fejlesztésében (bevezető): formális követelmény-specifikáció, modellezés, verifikáció (modellellenőrzés, helyességbizonyítás) szerepe. Mérnöki és formális modellek kapcsolata, modell-leképzések. Formális módszereket alkalmazó tervezőrendszerek (példák).
- Alapszintű formális modellek és szemantikájuk: Kripke struktúrák, tranzíciós rendszerek, Kripke tranzíciós rendszerek, időzített automaták és időzített 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*). A kifejezőképesség összehasonlítása.
- Formális
verifikáció modellellenőrzéssel: Modellellenőrzés tabló módszerrel, valamint
szimbolikus technikákkal. Időfüggő viselkedés ellenőrzése.
Kijelölt írásos tananyag: Tutorial on UPPAAL. https://uppaal.org/documentation/ - Nagyméretű állapottérrel rendelkező modellek verifikációja: Az állapottér kezelése döntési diagramok használatával. Korlátos modellellenőrzés.
- Gyakorlati alkalmazások: Beágyazott vezérlők és protokollok modellezése időzített automatákkal, temporális követelmények ellenőrzése az UPPAAL modellellenőrző használatával. Automatikus tesztgenerálás modellellenőrzővel. Monitor szintézis temporális logikai követelmények alapján.
- Állapotfüggő viselkedés magas szintű modellezése: Állapottérképek formális szemantikája. Tervezés állapottérképek használatával, az állapottérképek verifikációja. Az állapottérkép alapú forráskód szintézis elterjedt megoldásai.
- Konkurens rendszerek modellezése és viselkedési tulajdonságainak vizsgálata: A Petri háló formalizmus. Modellek dinamikus tulajdonságainak (holtpontmentesség, élőség, korlátosság, perzisztencia, visszatérő állapotok) ellenőrzése szimulációval és az elérhetőségi gráf alapján. Hierarchikus Petri hálók. Modellezési mintapéldák.
- Konkurens rendszerek strukturális tulajdonságainak vizsgálata: Állapotokra és viselkedésre vonatkozó invariánsok, strukturális korlátosság és vezérelhetőség kifejezése és ellenőrzése. Tulajdonságmegőrző modell-redukciós technikák.
- Adatfüggő viselkedés modellezése: Adattípusok és adatkezelés modellezése. A dinamikus és strukturális tulajdonságok kiterjesztése. Gyakorlati alkalmazások: Elosztott adatkezelés konzisztenciájának vizsgálata, protokollok analízise.
- Extra-funkcionális tulajdonságok specifikálása és verifikációja: A Petri hálók kiterjesztése valószínűségi és idő jellemzőkkel: sztochasztikus Petri hálók. Követelmények formalizálása sztochasztikus analízishez, teljesítmény és megbízhatósági tulajdonságok vizsgálata.
- Modellfinomítás: A szisztematikus modellfinomítás módszerei. A modellfinomítás konzisztenciájának ellenőrzése a viselkedésre vonatkozó relációk használatával.
- Szoftver forráskód alapú formális verifikációs technikák: Modellellenőrzés C programokon. Absztrakció használata: statikus analízis absztrakt interpretációval, predikátum absztrakció, ellenpélda vezérelt absztrakció finomítás a modellellenőrzés során.
- Program helyességbizonyítás: Kontraktusok, elő- és utófeltételek, invariánsok formalizálása, ellenőrzésük az algoritmusok magas szintű leírása illetve köztes reprezentációja alapján.
Az informatikai rendszerek bonyolultságának és a potenciális hibák kockázatának növekedésével mindinkább elvárás az, hogy a kritikus funkciók tervezése és megvalósítása bizonyítottan helyes (hibamentes) legyen. Ennek egyik jellegzetes megoldása a formális módszereket alkalmazó fejlesztés: formális modellek biztosítják a követelmények és tervek egyértelmű és precíz rögzítését, formális verifikációval vizsgálhatók a tervezői döntések és bizonyíthatók a tervek egyes tulajdonságai, az ellenőrzött tervek pedig alapját képezhetik a forráskód szintézisnek. 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 modellezési nyelveket, valamint a kapcsolódó analitikus és szimulációs vizsgálati módszereket. A tárgy demonstrálja a formális módszerek alkalmazását a követelmény-specifikáció, a rendszer- és szoftvertervezés, a modell alapú verifikáció, valamint a forráskód szintézis területén.
A tantárgy követelményeit eredményesen teljesítő hallgatók (1) megismernek és alkalmazni tudnak különböző formális módszereket, (2) képesek lesznek nem-formális rendszerleírások alapján formális modellt alkotni, (3) tisztában lesznek a formális verifikációs technikák előnyeivel és korlátaival, (4) megismernek formális módszereket támogató alapvető eszközöket.
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. Második kiadás, TypoTeX Kiadó, 2006.Bartha Tamás, Majzik István: Biztonságra tervezés és biztonságigazolás formális módszerei. Akadémiai Kiadó, 2019.E. M. Clarke, O. Grumberg, D. Kroening, D. Peled, H. Veith: Model Checking. 2nd edition, MIT Press, 2018. ISBN 9780262038836
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)
Programozás
alapjai, digitális technika
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)
Programozás
alapjai, digitális technika
Általános szabályok
Követelmények:
A félévközi jegy megszerzésének követelménye két zárthelyi legalább elégséges szintű teljesítése. Sikeres zárthelyik jegye egy-egy jeggyel javítható opcionális modellezési és verifikációs (otthoni) feladatok megoldásával. A félévközi jegyet 50%-50%-os súllyal a két zárthelyi osztályzata határozza meg.
Pótlási lehetőségek:
A szorgalmi időszak során minden zárthelyi dolgozathoz tartozik egy pótzárthelyi alkalom. Ez felhasználható az elmulasztott vagy sikertelen zárthelyi pótlására, vagy a sikeres zárthelyi eredményének javítására. A pótzárthelyi eredménye felülírja a korábbi eredményt - akkor is, ha az rosszabb, mint a korábbi.
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.